lean4-htt/library/init/meta
2016-06-07 17:51:04 -07:00
..
base_tactic.lean chore(library/init/meta/base_tactic): exception takes 'options' 2016-06-07 09:54:50 -07:00
declaration.lean feat(library/vm): expose 'environment' C++ object 2016-06-07 17:01:17 -07:00
default.lean feat(library/vm): expose 'environment' C++ object 2016-06-07 17:01:17 -07:00
environment.lean feat(library/vm): expose 'environment' C++ object 2016-06-07 17:01:17 -07:00
exceptional.lean feat(library/vm): expose 'environment' C++ object 2016-06-07 17:01:17 -07:00
expr.lean refactor(library/init): cmp_result => ordering 2016-06-07 10:14:07 -07:00
format.lean feat(library/vm/vm_environment): add rest of environment API 2016-06-07 17:51:04 -07:00
level.lean refactor(library/init): cmp_result => ordering 2016-06-07 10:14:07 -07:00
name.lean refactor(library/init): cmp_result => ordering 2016-06-07 10:14:07 -07:00
options.lean refactor(library): move 'meta' to 'init' folder 2016-06-06 19:08:07 -07:00
rb_map.lean refactor(library/init): cmp_result => ordering 2016-06-07 10:14:07 -07:00