mathlib documentation

core / init.data.sum.basic

@[protected, instance]
def sum.inhabited_left {α : Type u} {β : Type v} [h : inhabited α] :
inhabited β)
Equations
@[protected, instance]
def sum.inhabited_right {α : Type u} {β : Type v} [h : inhabited β] :
inhabited β)
Equations