| .. |
|
AC
|
refactor: remove duplication MVarId.applyRefl => MVarId.refl
|
2022-08-01 18:44:07 -07:00 |
|
LinearArith
|
refactor: use computed fields for Expr
|
2022-07-11 14:19:41 -07:00 |
|
Simp
|
feat: add missingDocs linter
|
2022-07-31 18:18:21 -07:00 |
|
AC.lean
|
refactor: move ac proofs to Init.
|
2022-03-16 17:21:20 -07:00 |
|
Acyclic.lean
|
refactor: improve MVarId method discoverability
|
2022-07-27 17:49:00 -07:00 |
|
Apply.lean
|
refactor: remove duplication MVarId.applyRefl => MVarId.refl
|
2022-08-01 18:44:07 -07:00 |
|
Assert.lean
|
refactor: improve FVarId method discoverability
|
2022-07-25 22:18:58 -07:00 |
|
Assumption.lean
|
refactor: improve MVarId method discoverability
|
2022-07-24 21:36:33 -07:00 |
|
AuxLemma.lean
|
feat: add field all to DefinitionVal and TheoremVal
|
2022-06-23 16:13:26 -07:00 |
|
Cases.lean
|
refactor: improve MVarId method discoverability
|
2022-07-27 17:49:00 -07:00 |
|
Cleanup.lean
|
refactor: improve FVarId method discoverability
|
2022-07-25 22:18:58 -07:00 |
|
Clear.lean
|
refactor: improve MVarId method discoverability
|
2022-07-24 21:36:33 -07:00 |
|
Congr.lean
|
feat: avoid [Decidable p] instance implicit parameters in congruence theorems when possible
|
2022-08-02 04:47:42 -07:00 |
|
Constructor.lean
|
refactor: improve MVarId method discoverability
|
2022-07-24 21:36:33 -07:00 |
|
Contradiction.lean
|
refactor: improve MVarId method discoverability
|
2022-07-27 17:49:00 -07:00 |
|
Delta.lean
|
refactor: improve MVarId method discoverability
|
2022-07-24 21:36:33 -07:00 |
|
ElimInfo.lean
|
refactor: improve FVarId method discoverability
|
2022-07-25 22:18:58 -07:00 |
|
FVarSubst.lean
|
chore: convert doc/mod comments from /- to /--//-! (#1354)
|
2022-07-22 12:05:31 -07:00 |
|
Generalize.lean
|
refactor: improve MVarId method discoverability
|
2022-07-27 17:49:00 -07:00 |
|
Induction.lean
|
refactor: add doc strings, cleanup, and dotted notation friendly API
|
2022-07-27 16:01:15 -07:00 |
|
Injection.lean
|
refactor: improve FVarId method discoverability
|
2022-07-25 22:18:58 -07:00 |
|
Intro.lean
|
fix: make forall_congr more robust at conv intro
|
2022-08-05 12:38:49 -07:00 |
|
LinearArith.lean
|
feat: basic support for linear Nat arithmetic at simp
|
2022-02-26 08:58:32 -08:00 |
|
Refl.lean
|
refactor: remove duplication MVarId.applyRefl => MVarId.refl
|
2022-08-01 18:44:07 -07:00 |
|
Rename.lean
|
refactor: improve MVarId method discoverability
|
2022-07-24 21:36:33 -07:00 |
|
Replace.lean
|
refactor: improve FVarId method discoverability
|
2022-07-25 22:18:58 -07:00 |
|
Revert.lean
|
refactor: improve FVarId method discoverability
|
2022-07-25 22:18:58 -07:00 |
|
Rewrite.lean
|
refactor: improve MVarId method discoverability
|
2022-07-24 21:36:33 -07:00 |
|
Simp.lean
|
refactor: CongrLemma => SimpCongrTheorem
|
2022-02-06 09:15:39 -08:00 |
|
Split.lean
|
refactor: improve MVarId method discoverability
|
2022-07-24 21:36:33 -07:00 |
|
SplitIf.lean
|
refactor: improve MVarId method discoverability
|
2022-07-27 17:49:00 -07:00 |
|
Subst.lean
|
refactor: improve FVarId method discoverability
|
2022-07-25 22:18:58 -07:00 |
|
Unfold.lean
|
refactor: improve FVarId method discoverability
|
2022-07-25 22:18:58 -07:00 |
|
UnifyEq.lean
|
refactor: improve FVarId method discoverability
|
2022-07-25 22:18:58 -07:00 |
|
Util.lean
|
feat: use infer_instance to close remaining goals at conv block
|
2022-08-02 04:24:56 -07:00 |
