Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-16 20:17 9f6bcd09

View on Github →

refactor(data/bool): decidable forall bool

Estimated changes

Modified data/bool.lean

deleted theorem bool.absurd_of_eq_ff_of_eq_tt

modified theorem bool.band_assoc

modified theorem bool.band_comm

modified theorem bool.band_elim_left

modified theorem bool.band_elim_right

modified theorem bool.band_intro

modified theorem bool.band_left_comm

modified theorem bool.bor_assoc

modified theorem bool.bor_comm

modified theorem bool.bor_left_comm

modified theorem bool.bxor_assoc

modified theorem bool.bxor_comm

modified theorem bool.bxor_left_comm

modified theorem bool.eq_ff_of_bnot_eq_tt

modified theorem bool.eq_ff_of_ne_tt

modified theorem bool.eq_tt_of_bnot_eq_ff

modified theorem bool.eq_tt_of_ne_ff

added theorem bool.exists_bool

added theorem bool.forall_bool