Leonardo de Moura 5adadc3158 test: document let issue ... TODO: fix issue at `Meta.mkLambda` when some of the free variables are let-declarations.		2019-12-19 17:29:26 -08:00
..
Compiler	chore: naming convention	2019-12-15 18:28:00 -08:00
Data	chore: naming convention	2019-12-15 18:28:00 -08:00
Elab	test: document let issue	2019-12-19 17:29:26 -08:00
EqnCompiler
Meta	fix: isDefEqQuick	2019-12-19 11:10:58 -08:00
Parser	feat: $. notation	2019-12-19 14:03:27 -08:00
Util	fix: typo	2019-12-19 12:03:13 -08:00
Attributes.lean	chore: naming convention	2019-12-15 18:28:00 -08:00
AuxRecursor.lean
Class.lean	chore: naming convention	2019-12-15 18:28:00 -08:00
Compiler.lean
Declaration.lean	chore: add instances	2019-12-12 08:19:38 -08:00
Elab.lean	refactor: split Elab/Term.lean into smaller files	2019-12-19 07:26:54 -08:00
Environment.lean	chore: naming convention	2019-12-15 18:28:00 -08:00
EqnCompiler.lean
Eval.lean	chore: avoid ^do ...	2019-12-11 06:19:12 -08:00
Expr.lean	chore: naming convention	2019-12-15 07:40:32 -08:00
Hygiene.lean	refactor: use match_syntax to implement expandCDot	2019-12-19 06:34:52 -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: naming convention	2019-12-15 18:28:00 -08:00
Meta.lean	feat: add user-friendly Meta.Exception -> MessageData	2019-12-10 15:49:52 -08:00
MetavarContext.lean	feat: split synthetic into synthetic and syntheticOpaque	2019-12-16 17:06:45 -08:00
Modifiers.lean
Parser.lean
ProjFns.lean	chore: naming convention	2019-12-15 07:48:42 -08:00
ReducibilityAttrs.lean
Runtime.lean
Scopes.lean
Structure.lean	chore: naming convention	2019-12-15 07:48:42 -08:00
Syntax.lean	feat: match_syntax support in the old parser	2019-12-17 12:16:34 -08:00
ToExpr.lean	chore: remove mkCApp* functions	2019-12-04 13:07:42 -08:00