]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/ng_assembly2/emulator/opcodes/pseudo.ma
mod change (-x)
[helm.git] / helm / software / matita / contribs / ng_assembly2 / emulator / opcodes / pseudo.ma
old mode 100755 (executable)
new mode 100644 (file)
index c881965..4c5e3af
@@ -139,7 +139,7 @@ unification hint 0 ≔ M:mcu_type ⊢ carr (im_is_comparable M) ≡ aux_im_type
 (* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
 (* ********************************************* *)
 
-ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_pseudo_type mcu) (aux_im_type mcu) byte8_or_word16 byte8.
+ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_pseudo_type mcu) (aux_im_type mcu) byte8_or_word16 nat.
 
 (* su tutta la lista quante volte compare il byte *)
 nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:word16) (l:list (aux_table_type m)) on l ≝