Commit 2022-10-25 22:36 44c394bb

View on Github →

feat(data/bool/basic): add several lemmas (#17153) Also rename bool.bnot_false/bool.bnot_true to more predictable names bool.bnot_ff/bool.bnot_tt.

Estimated changes

Modified src/data/bool/basic.lean

added theorem bool.bnot_eq_iff

deleted theorem bool.bnot_false

added theorem bool.bnot_ff

added theorem bool.bnot_ne_self

deleted theorem bool.bnot_true

added theorem bool.bnot_tt

added theorem bool.eq_bnot_iff

modified theorem bool.eq_ff_of_bnot_eq_tt

added theorem bool.eq_or_eq_bnot

modified theorem bool.eq_tt_of_bnot_eq_ff

added theorem bool.self_ne_bnot

modified theorem bool.to_bool_not