Sunbelt Computer Software

PL/B Language Development and Support

core / init.data.sum.basic - mathlib3 docs

mathlib3 documentation

core / init.data.sum.basic

@[protected, instance]

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

inhabited (α ⊕ β)

Equations

sum.inhabited_left = {default := sum.inl inhabited.default}

@[protected, instance]

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

inhabited (α ⊕ β)

Equations

sum.inhabited_right = {default := sum.inr inhabited.default}