lean4-htt/library/init/lean/elaborator
2019-07-17 19:09:16 -07:00
..
basic.lean feat(library/init/lean/elaborator/basic): add [builtinTermElab] attribute 2019-07-17 19:09:16 -07:00
default.lean feat(library/init/lean/elaborator): add Elab monad 2019-07-17 19:09:16 -07:00
elabstrategyattrs.lean