Leonardo de Moura 2387f3c2a2 feat(library/init/lean/elaborator): improve namespace, scope, and end commands		2019-07-22 08:14:35 -07:00
..
basic.lean	feat(library/init/lean/elaborator): improve namespace, scope, and end commands	2019-07-22 08:14:35 -07:00
command.lean	feat(library/init/lean/elaborator): improve namespace, scope, and end commands	2019-07-22 08:14:35 -07:00
default.lean	feat(library/init/lean/elaborator): use SyntaxNode to define TermElab and CommandElab	2019-07-21 07:29:41 -07:00
elabstrategyattrs.lean	feat(library/init/lean/elaborator): implement elaborator strategy attributes in Lean	2019-06-25 08:24:56 -07:00