fixed includes and added notation for bytes

[helm.git] / matita / library / assembly / vm.ma

diff --git a/matita/library/assembly/vm.ma b/matita/library/assembly/vm.ma
index 239146a07526445c12d662592117e32c26358b2e..162b5df0f378cf8f28e096b56a02feba9fbe481f 100644 (file)
--- a/matita/library/assembly/vm.ma
+++ b/matita/library/assembly/vm.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/assembly/vm/".
 
-include "byte.ma".
+include "assembly/byte.ma".
 
 definition addr ≝ nat.
 
@@ -95,6 +95,12 @@ definition byte_of_opcode : opcode → byte ≝
   in
    aux opcodemap.
 
+notation "hvbox(# break a)"
+  non associative with precedence 80
+for @{ 'byte_of_opcode $a }.
+interpretation "byte_of_opcode" 'byte_of_opcode a =
+ (cic:/matita/assembly/vm/byte_of_opcode.con a).
+
 record status : Type ≝ {
   acc : byte;
   pc  : addr;