lean4-htt/src/library/vm
Leonardo de Moura fd1141d999 fix(library/vm/vm,library/compiler/vm_compiler): invoke n ==> apply
This change fixes a bug in the VM and simplifies the VM instruction semantics.
2016-05-23 16:45:42 -07:00
..
CMakeLists.txt feat(library/vm/optimize): add basic bytecode optimizations 2016-05-12 15:24:58 -07:00
init_module.cpp
init_module.h
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 fix(library/vm/vm,library/compiler/vm_compiler): invoke n ==> apply 2016-05-23 16:45:42 -07:00
vm.h fix(library/vm/vm,library/compiler/vm_compiler): invoke n ==> apply 2016-05-23 16:45:42 -07:00
vm_nat.cpp feat(frontends/lean/decl_cmds): do not generate warning for definitions that are implemented in the VM 2016-05-13 18:17:20 -07:00
vm_nat.h