Sebastian Ullrich 92380ec5bd feat: implement MetaHasEval for MetaM		2019-12-05 13:20:24 +01:00
..
AbstractMVars.lean	feat: missing methods	2019-12-03 09:09:45 -08:00
AppBuilder.lean	feat: add mkAppM	2019-12-04 16:12:24 -08:00
Basic.lean	feat: implement MetaHasEval for MetaM	2019-12-05 13:20:24 +01:00
Check.lean	feat: ensure trace messages at MetaM save Environment, MetavarContext, and LocalContext	2019-11-22 11:50:19 -08:00
DiscrTree.lean	fix: use eta reduction at DiscrTree	2019-12-03 10:30:53 -08:00
DiscrTreeTypes.lean	feat: add synthInstance cache	2019-12-01 18:32:48 -08:00
Exception.lean	chore: move helper modules to src/Init/Lean/Util	2019-12-04 17:17:34 -08:00
ExprDefEq.lean	fix: accidental variable shadowing	2019-12-03 14:38:59 -08:00
FunInfo.lean	chore: remove ParamInfo.proof field	2019-11-25 08:42:23 -08:00
InferType.lean	chore: move Lean auxiliary datatypes to src/Init/Lean/Data	2019-12-04 17:00:13 -08:00
Instances.lean	feat: add generate, newSubgoal, tryResolve, and simpler table	2019-12-02 19:00:43 -08:00
LevelDefEq.lean	feat: add isLevelDefEqStuck exception	2019-12-01 18:42:33 -08:00
Offset.lean	chore: move Lean auxiliary datatypes to src/Init/Lean/Data	2019-12-04 17:00:13 -08:00
Reduce.lean	feat: add reduce	2019-11-25 08:42:23 -08:00
SynthInstance.lean	fix: caching condition	2019-12-04 16:14:26 -08:00
WHNF.lean	chore: move helper modules to src/Init/Lean/Util	2019-12-04 17:17:34 -08:00