lean4-htt/src/library/vm
2016-11-14 17:25:25 -08:00
..
CMakeLists.txt refactor(library): move user_attribute to tactic folder 2016-08-26 09:28:42 -07:00
init_module.cpp refactor(library): move user_attribute to tactic folder 2016-08-26 09:28:42 -07:00
init_module.h refactor(library): move vm to a separate directory 2016-05-12 14:45:06 -07:00
optimize.cpp fix(library/vm/optimize): bytecode optimization 2016-05-23 14:35:10 -07:00
optimize.h feat(library/vm/optimize): add basic bytecode optimizations 2016-05-12 15:24:58 -07:00
vm.cpp feat(library/vm,library/tactic/vm_monitor): use optionT to define vm monad 2016-11-14 16:13:56 -08:00
vm.h feat(library/tactic/vm_monitor): add VM introspection API 2016-11-14 17:25:25 -08:00
vm_aux.cpp feat(library/vm): add 'trace' 2016-06-08 16:32:20 -07:00
vm_aux.h feat(library/vm,library/init): add builtin timeit primitive for profiling 2016-05-26 12:44:49 -07:00
vm_declaration.cpp fix(library/vm/vm_declaration): fix typo in instantiate_value_univ_params 2016-10-06 21:34:00 -07:00
vm_declaration.h feat(library/vm): expose 'declaration' C++ object 2016-06-07 15:38:48 -07:00
vm_environment.cpp chore(*): fix style errors 2016-11-04 09:47:17 -07:00
vm_environment.h feat(library/vm): expose 'environment' C++ object 2016-06-07 17:01:17 -07:00
vm_exceptional.cpp feat(library/vm/vm_exceptional): handle formatted_exception 2016-09-25 18:52:13 -07:00
vm_exceptional.h feat(library/tactic/tactic_state): add basic tactics for inferring types, unifying terms, etc 2016-06-11 10:51:33 -07:00
vm_expr.cpp feat(library/vm): add expr.copy_pos_info 2016-11-10 11:50:38 -08:00
vm_expr.h refactor(library/tactic/simplify): add simplify subclasses, and use new simplifier at nested 2016-10-18 16:18:25 -07:00
vm_format.cpp chore(library/vm,library/tactic): fix warnings produced by the new clang++ 2016-09-25 11:14:28 -07:00
vm_format.h feat(library/vm/vm_format,library/tactic): use thunks unit->format when producing error messages 2016-08-04 19:19:09 -07:00
vm_io.cpp fix(library/vm/vm_io): disable get_line in server mode 2016-10-19 10:02:58 -07:00
vm_io.h feat(library/vm): add basic support for IO monad 2016-05-24 17:52:22 -07:00
vm_level.cpp chore(library/vm,library/tactic): fix warnings produced by the new clang++ 2016-09-25 11:14:28 -07:00
vm_level.h feat(library/vm): avoid list<A> eager conversion to vm_obj (for A in {name, level, expr}) 2016-06-09 14:16:32 -07:00
vm_list.cpp chore(library/vm,library/tactic): fix warnings produced by the new clang++ 2016-09-25 11:14:28 -07:00
vm_list.h feat(library/vm/vm_list): add to_list 2016-07-17 14:34:47 -04:00
vm_name.cpp chore(library/vm,library/tactic): fix warnings produced by the new clang++ 2016-09-25 11:14:28 -07:00
vm_name.h feat(library/vm): avoid list<A> eager conversion to vm_obj (for A in {name, level, expr}) 2016-06-09 14:16:32 -07:00
vm_nat.cpp feat(library/vm): expose 'environment' C++ object 2016-06-07 17:01:17 -07:00
vm_nat.h feat(library/vm): expose 'environment' C++ object 2016-06-07 17:01:17 -07:00
vm_option.h feat(library/tactic/app_builder_tactics): add tactic.mk_mapp 2016-06-14 17:33:32 -07:00
vm_options.cpp chore(library/vm,library/tactic): fix warnings produced by the new clang++ 2016-09-25 11:14:28 -07:00
vm_options.h feat(library/vm): expose C++ options object 2016-06-02 11:46:17 -07:00
vm_ordering.h refactor(library/init): cmp_result => ordering 2016-06-07 10:14:07 -07:00
vm_pexpr.cpp feat(frontends/lean): improve 'begin...end' blocks 2016-09-27 13:34:11 -07:00
vm_pexpr.h refactor(library/init/meta): qexpr ==> pexpr 2016-08-05 17:04:36 -07:00
vm_rb_map.cpp chore(library/vm,library/tactic): fix warnings produced by the new clang++ 2016-09-25 11:14:28 -07:00
vm_rb_map.h feat(library/vm): expose rb_map object 2016-06-03 13:45:06 -07:00
vm_string.cpp chore(library/vm): style 2016-05-26 12:57:34 -07:00
vm_string.h refactor(library/vm): move vm_obj <=> string conversion functions to separate module 2016-05-26 10:47:19 -07:00