This file contains WellFoundedRelation instances Bool.

They are provided as defs rather than instances, despite WellFoundedRelation being a class, as we provide versions for both < and >. If you need instances, you may use the WellFoundedLT and WellFoundedGT classes available in Mathlib.

@[implicit_reducible]

def Bool.lt_wfRel : WellFoundedRelation Bool

Boolean '<' is well founded

Equations

• Bool.lt_wfRel = { rel := fun (x1 x2 : Bool) => x1 < x2, wf := Bool.lt_wfRel._proof_1 }

@[implicit_reducible]

def Bool.gt_wfRel : WellFoundedRelation Bool

Boolean '>' is well founded

Equations

• Bool.gt_wfRel = { rel := fun (x1 x2 : Bool) => x1 > x2, wf := Bool.gt_wfRel._proof_1 }