mathlib documentation

core / init.data.sum.basic

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

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

Equations