pith. machine review for the scientific record. sign in
def definition def or abbrev

strictBooleanRealization

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  36def strictBooleanRealization : StrictLogicRealization where
  37  Carrier := Bool

proof body

Definition body.

  38  Cost := Nat
  39  zeroCost := inferInstance
  40  compare := boolCost
  41  compose := xorBool
  42  one := false
  43  generator := true
  44  identity_law := boolCost_self
  45  non_contradiction_law := boolCost_symm
  46  excluded_middle_law := True
  47  composition_law := True
  48  invariance_law := True
  49  nontrivial_law := by
  50    simp [boolCost]
  51
  52/-- Strict Boolean forced arithmetic is canonically `LogicNat`. -/

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (19)

Lean names referenced from this declaration's body.