Leonardo de Moura 8a249bddd2 feat: add try rfl at end of convTarget		2021-09-03 08:14:47 -07:00
..
Conv	feat: add try rfl at end of convTarget	2021-09-03 08:14:47 -07:00
Basic.lean	refactor: add annotation for displaying conv state	2021-09-02 15:52:11 -07:00
BuiltinTactic.lean	feat: case _ ... => ... as solve next goal	2021-08-29 10:45:38 -07:00
Conv.lean	feat: add 'change' conv tactic	2021-09-02 19:26:25 -07:00
ElabTerm.lean	feat: add 'change' conv tactic	2021-09-02 19:26:25 -07:00
Generalize.lean	feat: nary generalize tactic	2021-08-30 16:31:39 -07:00
Induction.lean	feat: nary generalize tactic	2021-08-30 16:31:39 -07:00
Injection.lean	feat: add injections tactic	2021-08-31 19:12:06 -07:00
Location.lean	fix: location notation and simp	2021-03-19 19:54:22 -07:00
Match.lean	feat: add (generalizing := true/false) optional attribute to match	2021-04-15 17:04:25 -07:00
Rewrite.lean	feat: add rewrite conv tactic	2021-09-02 18:13:19 -07:00
Simp.lean	fix: make sure simp only still uses eq_self	2021-08-30 09:50:11 -07:00
Split.lean	feat: add support for split at	2021-08-31 19:35:07 -07:00