lean4-htt/src/stage0
Leonardo de Moura 08cdb757b4 feat(library/init/lean/environment): add Environment.addAndCompile
To fix `BuiltinParserAttribute`, we need to be able to add auxiliary declarations programmatically.
2019-06-18 18:20:17 -07:00
..
init feat(library/init/lean/environment): add Environment.addAndCompile 2019-06-18 18:20:17 -07:00
.gitattributes
.gitignore chore(state0/.gitignore): ignore .o 2019-03-18 18:30:28 -07:00
CMakeLists.txt feat(library/compiler/init_attribute): switch to @[init] attribute in Lean 2019-06-18 16:03:52 -07:00