Equations
- Lean.instBEqLBool = { beq := [anonymous] }
Equations
- Lean.instInhabitedLBool = { default := Lean.LBool.false }
Equations
- Lean.LBool.neg x = match x with | Lean.LBool.true => Lean.LBool.false | Lean.LBool.false => Lean.LBool.true | Lean.LBool.undef => Lean.LBool.undef
Equations
- Lean.LBool.and x x = match x, x with | Lean.LBool.true, b => b | a, x => a
Equations
- Lean.LBool.toString x = match x with | Lean.LBool.true => "true" | Lean.LBool.false => "false" | Lean.LBool.undef => "undef"
Equations
- Lean.LBool.instToStringLBool = { toString := Lean.LBool.toString }
Equations
- Bool.toLBool x = match x with | true => Lean.LBool.true | false => Lean.LBool.false
@[inline]
Equations
- toLBoolM x = do let b ← x pure (Bool.toLBool b)