mathlib documentation

core / init.data.punit

theorem punit_eq (a b : punit) :
a = b
theorem punit_eq_star (a : punit) :
@[instance]
Equations