mathlib3 documentation

core / init.data.punit

theorem punit_eq (a b : punit) :

a = b

theorem punit_eq_star (a : punit) :

a = punit.star

@[protected, instance]

def punit.subsingleton :

subsingleton punit

@[protected, instance]

def punit.inhabited :

inhabited punit

Equations

punit.inhabited = {default := punit.star}

@[protected, instance]

def punit.decidable_eq :

decidable_eq punit

Equations

punit.decidable_eq = λ (a b : punit), decidable.is_true _