Commit 2021-08-03 14:34 78229266
View on Github →Few tactic implementations (#27)
- aligned tactic names to mathport
- added byContra tactic
- added guardExprEq guardTarget guardHyp
- added introv
- Update Mathlib/Tactic/Basic.lean
- Update Mathlib/Tactic/Basic.lean
- added exacts
- use of elab and examples
- matchTarget
- byContra all cases
- sorry & iterate
- fix : get to build
- fix : get to build
- fix : get to build 3