mathlib documentation

core.init.data.sum.basic

@[instance]

def sum.inhabited_left {α : Type u} {β : Type v} [h : inhabited α] :

inhabited (α ⊕ β)

Equations

sum.inhabited_left = {default := sum.inl (default α)}

@[instance]

def sum.inhabited_right {α : Type u} {β : Type v} [h : inhabited β] :

inhabited (α ⊕ β)

Equations

sum.inhabited_right = {default := sum.inr (default β)}