lean4-htt/src/Init/Lean
2019-12-09 15:22:25 -08:00
..
Compiler chore: move Lean auxiliary datatypes to src/Init/Lean/Data 2019-12-04 17:00:13 -08:00
Data feat: option declarations in Lean 2019-12-05 06:18:35 -08:00
Elab feat: register trace.Elab 2019-12-09 15:22:25 -08:00
EqnCompiler chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Meta refactor: MonadTracer and helper functions 2019-12-08 09:05:15 -08:00
Parser refactor: remove Syntax.other 2019-12-06 09:23:44 -08:00
Util feat: add tracingAt 2019-12-08 09:51:51 -08:00
Attributes.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
AuxRecursor.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Class.lean feat: add checkOutParam validation 2019-12-01 18:32:48 -08:00
Compiler.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Declaration.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Elab.lean feat: add basic commands 2019-12-07 17:55:31 -08:00
Environment.lean chore: move helper modules to src/Init/Lean/Util 2019-12-04 17:17:34 -08:00
EqnCompiler.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Eval.lean feat: add Lean.MetaHasEval, rename HasEval to Lean.HasEval 2019-12-05 13:20:24 +01:00
Expr.lean feat: add Expr.headBeta 2019-12-05 09:01:50 -08:00
Level.lean chore: move Lean auxiliary datatypes to src/Init/Lean/Data 2019-12-04 17:00:13 -08:00
Linter.lean chore: move helper modules to src/Init/Lean/Util 2019-12-04 17:17:34 -08:00
LocalContext.lean chore: add abbreviations MVarId and FVarId 2019-11-28 08:18:06 -08:00
Meta.lean feat: add runTermElabM 2019-12-08 07:48:40 -08:00
MetavarContext.lean chore: move helper modules to src/Init/Lean/Util 2019-12-04 17:17:34 -08:00
Modifiers.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Parser.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
ProjFns.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
ReducibilityAttrs.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Runtime.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Scopes.lean chore: library/Init ==> src/Init 2019-11-22 06:06:05 -08:00
Syntax.lean feat: elaborate binders 2019-12-08 17:59:11 -08:00
ToExpr.lean chore: remove mkCApp* functions 2019-12-04 13:07:42 -08:00