mathlib documentation

core.init.data.punit

theorem punit_eq (a b : punit) :

a = b

theorem punit_eq_punit (a : punit) :

a = ()

@[instance]

def punit.subsingleton :

subsingleton punit

@[instance]

def punit.inhabited :

inhabited punit

Equations

punit.inhabited = {default := ()}

@[instance]

def punit.decidable_eq :

decidable_eq punit

Equations

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