Leonardo de Moura e13a10fbf2 feat: elaborate explicit and implicit arguments		2019-12-11 09:04:26 -08:00
..
Compiler	chore: avoid ^do ...	2019-12-11 06:19:12 -08:00
Data	chore: avoid ^do ...	2019-12-11 06:19:12 -08:00
Elab	feat: elaborate explicit and implicit arguments	2019-12-11 09:04:26 -08:00
EqnCompiler
Meta	feat: elaborate explicit and implicit arguments	2019-12-11 09:04:26 -08:00
Parser	fix: mark choice as valid SyntaxNodeKind	2019-12-11 06:19:12 -08:00
Util	chore: avoid ^do ...	2019-12-11 06:19:12 -08:00
Attributes.lean	chore: avoid ^do ...	2019-12-11 06:19:12 -08:00
AuxRecursor.lean
Class.lean	feat: add checkOutParam validation	2019-12-01 18:32:48 -08:00
Compiler.lean
Declaration.lean
Elab.lean	feat: add basic commands	2019-12-07 17:55:31 -08:00
Environment.lean	chore: avoid ^do ...	2019-12-11 06:19:12 -08:00
EqnCompiler.lean
Eval.lean	chore: avoid ^do ...	2019-12-11 06:19:12 -08: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 user-friendly Meta.Exception -> MessageData	2019-12-10 15:49:52 -08:00
MetavarContext.lean	chore: avoid ^do ...	2019-12-11 06:19:12 -08:00
Modifiers.lean
Parser.lean
ProjFns.lean
ReducibilityAttrs.lean
Runtime.lean
Scopes.lean
Syntax.lean	feat: elabApp skeleton	2019-12-10 10:21:14 -08:00
ToExpr.lean	chore: remove mkCApp* functions	2019-12-04 13:07:42 -08:00