Booleans #
This file proves various trivial lemmas about booleans and their relation to decidable propositions.
Tags #
bool, boolean, Bool, De Morgan
De Morgan's laws for booleans #
Equations
- Bool.linearOrder = LinearOrder.mk Bool.linearOrder.proof_5 inferInstance inferInstance inferInstance Bool.linearOrder.proof_6 Bool.linearOrder.proof_7 Bool.linearOrder.proof_8
convert a ℕ
to a Bool
, 0 -> false
, everything else -> true
Equations
- Bool.ofNat n = decide (n ≠ 0)
Instances For
@[simp]