X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fassembly%2Fbyte.ma;h=583051e27c48ed1b0991eed43338358fbb0fedd2;hb=5a5debd7c094f392e84c2a0f7456321f26191499;hp=f97b13f293a131b4a2c7bb3b4c223aa37779e90d;hpb=61d5edd7f92c89bceae245453dead8cbd2a276b7;p=helm.git

diff --git a/matita/library/assembly/byte.ma b/matita/library/assembly/byte.ma
index f97b13f29..583051e27 100644
--- a/matita/library/assembly/byte.ma
+++ b/matita/library/assembly/byte.ma
@@ -42,6 +42,9 @@ coercion cic:/matita/assembly/byte/nat_of_byte.con.
 definition byte_of_nat ≝
  λn. mk_byte (exadecimal_of_nat (n / 16)) (exadecimal_of_nat n).
 
+interpretation "byte_of_nat" 'byte_of_opcode a =
+ (cic:/matita/assembly/byte/byte_of_nat.con a).
+
 lemma byte_of_nat_nat_of_byte: ∀b. byte_of_nat (nat_of_byte b) = b.
  intros;
  elim b;