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]
@[protected, instance]
Equations
@[protected, instance]
Equations