| .. |
|
Simp
|
feat: add mkInjectiveTheorems
|
2021-05-13 22:09:50 -07:00 |
|
Apply.lean
|
feat: use expected type to prioritize completion candidates
|
2021-04-03 14:12:42 -07:00 |
|
Assert.lean
|
fix: location notation and simp
|
2021-03-19 19:54:22 -07:00 |
|
Assumption.lean
|
refactor: add findLocalDeclWithType?
|
2021-03-03 15:44:32 -08:00 |
|
AuxLemma.lean
|
feat: add AuxLemma.lean
|
2021-03-09 18:25:19 -08:00 |
|
Cases.lean
|
fix: closes #421
|
2021-04-23 12:27:39 -07:00 |
|
Clear.lean
|
fix: location notation and simp
|
2021-03-19 19:54:22 -07:00 |
|
Constructor.lean
|
feat: add constructor tactic
|
2021-05-06 10:40:56 -07:00 |
|
Contradiction.lean
|
feat: contradiction catches empty inductive types
|
2021-03-21 21:48:43 -07:00 |
|
Delta.lean
|
chore: naming convention
|
2021-02-11 15:05:26 -08:00 |
|
ElimInfo.lean
|
fix: leftovers in the local context when applying induction
|
2021-03-27 19:42:22 -07:00 |
|
FVarSubst.lean
|
chore: use deriving Inhabited
|
2020-12-13 11:57:59 -08:00 |
|
Generalize.lean
|
chore: remove #lang lean4 header
|
2020-10-25 09:54:07 -07:00 |
|
Induction.lean
|
chore: trace[...]! ==> trace[...]
|
2021-03-10 18:44:43 -08:00 |
|
Injection.lean
|
chore: trace[...]! ==> trace[...]
|
2021-03-10 18:44:43 -08:00 |
|
Intro.lean
|
chore: rename option hygienicIntro ==> tactic.hygienic
|
2021-04-10 16:09:04 -07:00 |
|
Replace.lean
|
fix: ReplaceLocalDecl
|
2021-02-26 19:31:40 -08:00 |
|
Revert.lean
|
fix: fixes #310
|
2021-02-12 18:14:42 -08:00 |
|
Rewrite.lean
|
chore: update structure, class, inductive
|
2020-11-27 15:09:30 -08:00 |
|
Simp.lean
|
feat: add simp_all tactic
|
2021-03-19 22:34:35 -07:00 |
|
Subst.lean
|
feat: contradiction catches empty inductive types
|
2021-03-21 21:48:43 -07:00 |
|
Util.lean
|
refactor: add Name.modifyBase
|
2021-05-03 10:06:20 -07:00 |
