freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / translation.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
index b7fc76f7a51da4b39297f959dec7daeae1ab3282..0996948942bad7c8c8cd7b4809456eaa72acc96b 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
@@ -76,6 +76,12 @@ full_info_of_word16_aux m borw (opcode_table m).
 ninductive t_byte8 (m:mcu_type) : Type ≝
  TByte : byte8 → t_byte8 m.
 
+ndefinition eq_tbyte8 ≝
+λm.λtb1,tb2:t_byte8 m.
+ match tb1 with
+  [ TByte b1 ⇒ match tb2 with
+   [ TByte b2 ⇒ eq_b8 b1 b2 ]].
+
 (* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
 ninductive MA_check : instr_mode → Type ≝
   maINH              : MA_check MODE_INH