Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-10 00:01 e269dbc1

View on Github →

feat(tactic/itauto): Complete intuitionistic prover (#7057) As requested on Zulip.

Estimated changes

Modified docs/references.bib

Modified src/tactic/basic.lean

Created src/tactic/itauto.lean

added def tactic.itauto.and_kind.cmp

added def tactic.itauto.and_kind.sides

added inductive tactic.itauto.and_kind

added inductive tactic.itauto.proof

added def tactic.itauto.prop.and

added def tactic.itauto.prop.cmp

added def tactic.itauto.prop.eq

added def tactic.itauto.prop.iff

added def tactic.itauto.prop.not

added def tactic.itauto.prop.xor

added inductive tactic.itauto.prop

Created test/itauto.lean