lean4-htt/src/Init/Lean
2019-12-05 13:20:24 +01:00
..
Compiler chore: move Lean auxiliary datatypes to src/Init/Lean/Data 2019-12-04 17:00:13 -08:00
Data chore: move Lean auxiliary datatypes to src/Init/Lean/Data 2019-12-04 17:00:13 -08:00
Elaborator chore: move Lean auxiliary datatypes to src/Init/Lean/Data 2019-12-04 17:00:13 -08:00
EqnCompiler
Meta chore: move helper modules to src/Init/Lean/Util 2019-12-04 17:17:34 -08:00
Parser chore: move helper modules to src/Init/Lean/Util 2019-12-04 17:17:34 -08:00
Util chore: move helper modules to src/Init/Lean/Util 2019-12-04 17:17:34 -08:00
Attributes.lean
AuxRecursor.lean
Class.lean feat: add checkOutParam validation 2019-12-01 18:32:48 -08:00
Compiler.lean
Declaration.lean
Elaborator.lean
Environment.lean chore: move helper modules to src/Init/Lean/Util 2019-12-04 17:17:34 -08:00
EqnCompiler.lean
Eval.lean feat: add Lean.MetaHasEval, rename HasEval to Lean.HasEval 2019-12-05 13:20:24 +01:00
Expr.lean chore: move Lean auxiliary datatypes to src/Init/Lean/Data 2019-12-04 17:00:13 -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 helper functions 2019-12-04 12:43:24 -08:00
MetavarContext.lean chore: move helper modules to src/Init/Lean/Util 2019-12-04 17:17:34 -08:00
Modifiers.lean
Parser.lean
ProjFns.lean
ReducibilityAttrs.lean
Runtime.lean
Scopes.lean
Syntax.lean chore: move Lean auxiliary datatypes to src/Init/Lean/Data 2019-12-04 17:00:13 -08:00
ToExpr.lean chore: remove mkCApp* functions 2019-12-04 13:07:42 -08:00