lean4-htt/src/library/vm
2017-10-23 10:55:26 -07:00
..
CMakeLists.txt
init_module.cpp feat(library/vm/vm_string): provide native implementation of type string in the VM 2017-10-23 10:55:26 -07:00
init_module.h
interaction_state.h feat(library/tactic): add tactic::ref 2017-06-02 15:19:03 -07:00
interaction_state_imp.h feat(frontends/lean,shell/server): "hole" command 2017-06-14 21:56:17 -07:00
optimize.cpp
optimize.h
vm.cpp fix(library/vm/vm): bug at update_vm_constructor 2017-10-23 10:55:26 -07:00
vm.h feat(library/vm/vm_string): provide native implementation of type string in the VM 2017-10-23 10:55:26 -07:00
vm_array.cpp
vm_array.h
vm_aux.cpp
vm_aux.h
vm_declaration.cpp
vm_declaration.h
vm_environment.cpp feat(library/init/meta/environment): expose function to unfold all macros 2017-07-18 19:49:53 +01:00
vm_environment.h
vm_exceptional.cpp
vm_exceptional.h
vm_expr.cpp feat(kernel/expr): allow metavariables to have user-facing names 2017-07-16 07:16:41 -07:00
vm_expr.h refactor(init/meta/expr): unify expr and pexpr 2017-05-17 10:38:12 -07:00
vm_format.cpp
vm_format.h
vm_int.cpp fix(library/vm/vm_int): tons of fixes for int.shiftl 2017-07-11 22:54:26 +01:00
vm_int.h
vm_io.cpp refactor(*): wrap string in a structure 2017-06-07 17:30:49 -07:00
vm_io.h
vm_level.cpp fix(library): expr, level, hash_map, rb_map has_repr instances should be has_to_string since they do not produce results that can be parsed by Lean 2017-06-18 18:33:27 -07:00
vm_level.h
vm_list.cpp
vm_list.h
vm_name.cpp
vm_name.h
vm_nat.cpp feat(library/vm/vm_string): provide native implementation of type string in the VM 2017-10-23 10:55:26 -07:00
vm_nat.h feat(library/vm/vm_string): provide native implementation of type string in the VM 2017-10-23 10:55:26 -07:00
vm_native.cpp
vm_native.h
vm_option.h feat(init/meta/{interactive_base,parser}): decl_attributes, decl_meta_info, parser.set_env 2017-06-19 11:27:12 -07:00
vm_options.cpp
vm_options.h
vm_ordering.h
vm_parser.cpp feat(library/vm/vm_parser): expose parse_command_like to the vm 2017-08-14 11:41:48 +02:00
vm_parser.h feat(frontends/lean/user_command): add user-defined commands 2017-06-19 11:27:12 -07:00
vm_pexpr.cpp feat(init/meta/pexpr): allow creating structure instance pre-terms 2017-10-11 16:13:34 +02:00
vm_pexpr.h
vm_pos_info.cpp
vm_pos_info.h
vm_rb_map.cpp feat(library/init/meta/expr): add expr.has_local_in 2017-07-01 20:23:37 -07:00
vm_rb_map.h
vm_string.cpp fix(library/vm/vm_string): missing VM builtin for string_imp projections 2017-10-23 10:55:26 -07:00
vm_string.h feat(library/vm/vm_string): provide native implementation of type string in the VM 2017-10-23 10:55:26 -07:00
vm_task.cpp
vm_task.h