Script simplification due to the new efficient conversion strategy.

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

diff --git a/matita/library/assembly/byte.ma b/matita/library/assembly/byte.ma
index f97b13f293a131b4a2c7bb3b4c223aa37779e90d..583051e27c48ed1b0991eed43338358fbb0fedd2 100644 (file)
--- 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;