| .. |
|
Match
|
fix: equational lemma generation for definitions using named patterns
|
2022-01-19 17:45:54 -08:00 |
|
Tactic
|
chore: improve trace messages
|
2022-01-19 14:29:04 -08:00 |
|
AbstractMVars.lean
|
refactor: avoid Name, MVarId, and FVarId confusion
|
2021-09-07 19:06:50 -07:00 |
|
AbstractNestedProofs.lean
|
fix: preserve unused let declarations
|
2021-10-18 17:40:15 -07:00 |
|
AppBuilder.lean
|
chore: remove arbitrary
|
2022-01-15 12:14:27 -08:00 |
|
Basic.lean
|
chore: remove arbitrary
|
2022-01-15 12:14:27 -08:00 |
|
Check.lean
|
refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files
|
2021-12-06 09:57:00 -08:00 |
|
Closure.lean
|
chore: remove arbitrary
|
2022-01-15 12:14:27 -08:00 |
|
Coe.lean
|
feat: unfold coercions and coeFun, coeSort, coeM, liftCoeM
|
2021-02-14 10:27:34 -08:00 |
|
CollectFVars.lean
|
refactor: Lean.Meta should not depend on Lean.Elab
|
2021-12-06 08:05:24 -08:00 |
|
CollectMVars.lean
|
|
|
|
CongrTheorems.lean
|
chore: fix codebase
|
2021-12-10 13:12:09 -08:00 |
|
Constructions.lean
|
feat: optimized noConfusion for enumeration types
|
2021-09-06 11:52:36 -07:00 |
|
DecLevel.lean
|
refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files
|
2021-12-06 09:57:00 -08:00 |
|
DiscrTree.lean
|
chore: remove arbitrary
|
2022-01-15 12:14:27 -08:00 |
|
DiscrTreeTypes.lean
|
feat: add support for kernel projections to DiscrTree
|
2021-07-29 16:59:47 -07:00 |
|
Eqns.lean
|
feat: equation theorem manager
|
2021-09-17 14:20:28 -07:00 |
|
ExprDefEq.lean
|
chore: remove some [specialize] annotations
|
2022-01-18 09:24:06 -08:00 |
|
ForEachExpr.lean
|
|
|
|
FunInfo.lean
|
feat: add FunInfo.getArity
|
2021-09-14 15:58:00 -07:00 |
|
GeneralizeTelescope.lean
|
refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files
|
2021-12-06 09:57:00 -08:00 |
|
GeneralizeVars.lean
|
refactor: add sortFVarIds to Meta/Basic.lean
|
2021-09-20 11:32:53 -07:00 |
|
GetConst.lean
|
fix: ensure match-expressions compiled using if-then-else can be reduced with TransparencyMode.reducible
|
2021-12-18 10:55:42 -08:00 |
|
GlobalInstances.lean
|
refactor: break DiscrTree -> WHNF dependency
|
2021-07-29 15:26:35 -07:00 |
|
IndPredBelow.lean
|
feat: add equality proof for named patterns
|
2022-01-18 12:43:01 -08:00 |
|
Inductive.lean
|
refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files
|
2021-12-06 09:57:00 -08:00 |
|
InferType.lean
|
refactor: avoid Name, MVarId, and FVarId confusion
|
2021-09-07 19:06:50 -07:00 |
|
Injective.lean
|
chore: fix codebase
|
2021-12-10 13:12:09 -08:00 |
|
Instances.lean
|
feat: allow instances to be (temporarily) erased
|
2021-08-31 15:30:29 -07:00 |
|
KAbstract.lean
|
refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files
|
2021-12-06 09:57:00 -08:00 |
|
LevelDefEq.lean
|
refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files
|
2021-12-06 09:57:00 -08:00 |
|
Match.lean
|
chore: move MatchEqs
|
2021-08-17 21:32:32 -07:00 |
|
MatchUtil.lean
|
feat: add contradiction
|
2021-03-03 17:00:54 -08:00 |
|
Offset.lean
|
fix: bug at Offset.lean
|
2021-11-08 18:27:25 -08:00 |
|
PPGoal.lean
|
chore: fix codebase
|
2021-12-10 13:12:09 -08:00 |
|
RecursorInfo.lean
|
refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files
|
2021-12-06 09:57:00 -08:00 |
|
Reduce.lean
|
feat: add reduce conv tactic
|
2021-09-09 17:47:10 -07:00 |
|
ReduceEval.lean
|
chore: fix module comments, they must occur after the imports
|
2021-08-06 14:02:42 -07:00 |
|
SizeOf.lean
|
feat: add sizeOf spec lemmas as simp theorems
|
2022-01-17 16:14:38 -08:00 |
|
SortLocalDecls.lean
|
refactor: avoid Name, MVarId, and FVarId confusion
|
2021-09-07 19:06:50 -07:00 |
|
Structure.lean
|
fix: diamonds with dependent fields
|
2021-08-09 19:01:08 -07:00 |
|
SynthInstance.lean
|
chore: remove arbitrary
|
2022-01-15 12:14:27 -08:00 |
|
Tactic.lean
|
feat: add Meta.rename tactic
|
2022-01-12 16:15:30 -08:00 |
|
Transform.lean
|
fix: another instance of the binder cache issue
|
2021-05-05 10:45:38 -07:00 |
|
TransparencyMode.lean
|
feat: add Meta.Rewrite.Config
|
2021-09-12 18:44:08 -07:00 |
|
UnificationHint.lean
|
refactor: ExprDefEq.lean and LevelDefEq.lean are now implementation only files
|
2021-12-06 09:57:00 -08:00 |
|
WHNF.lean
|
feat: use getEqnsFor? at simp
|
2022-01-05 11:28:24 -08:00 |
