max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Meta
History
Leonardo de Moura 15cca3000a fix: withIncRecDepth was not aborting simp 
It was just making it stop simplification at the current branch.

Now, elaboration is interrupted after a few seconds in the example at
issue #906.

see #906
2022-01-26 07:48:58 -08:00
..
Match fix: mkEquationsFor at Match/MatchEqs.lean 2022-01-25 18:43:51 -08:00
Tactic fix: withIncRecDepth was not aborting simp 2022-01-26 07:48:58 -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
ACLt.lean chore: remove the now incorrect comment 2022-01-24 19:05:05 -08: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 chore: rename coeM and liftCoeM 2022-01-20 15:33:17 -08:00
CollectFVars.lean refactor: Lean.Meta should not depend on Lean.Elab 2021-12-06 08:05:24 -08:00
CollectMVars.lean chore: remove "liftable methods" 2020-12-09 15:06:07 -08:00
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 chore: remove unnecessary do 2021-01-26 12:41:07 -08:00
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 chore: add matchHEq? 2022-01-25 18:43:51 -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 fix: trace message with incorrect MetavarContext 2022-01-24 10:34:44 -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