Equations
- Lean.instInhabitedLBool = { default := Lean.LBool.false }
Equations
- Lean.instBEqLBool = { beq := Lean.beqLBool✝ }
Equations
- x.neg = match x with | Lean.LBool.true => Lean.LBool.false | Lean.LBool.false => Lean.LBool.true | Lean.LBool.undef => Lean.LBool.undef
Instances For
Equations
- x✝.and x = match x✝, x with | Lean.LBool.true, b => b | a, x => a
Instances For
Equations
- x.toString = match x with | Lean.LBool.true => "true" | Lean.LBool.false => "false" | Lean.LBool.undef => "undef"
Instances For
Equations
- Lean.LBool.instToString = { toString := Lean.LBool.toString }
Equations
- x.toLBool = match x with | true => Lean.LBool.true | false => Lean.LBool.false