(* -------------------------- *)
(* inizializzatori: ... valori ... *)
-inductive preast_init_val : Type ≝
+ninductive preast_init_val : Type ≝
PREAST_INIT_VAL_BYTE8: byte8 → preast_init_val
| PREAST_INIT_VAL_WORD16: word16 → preast_init_val
| PREAST_INIT_VAL_WORD32: word32 → preast_init_val
1) var1 = var2
2) var = ... valori ...
*)
-inductive preast_init : Type ≝
+ninductive preast_init : Type ≝
PREAST_INIT_VAR: preast_var → preast_init
| PREAST_INIT_VAL: preast_init_val → preast_init.
(* -------------------------- *)
(* statement: assegnamento/while/if else if else *)
-inductive preast_stm : Type ≝
+ninductive preast_stm : Type ≝
PREAST_STM_ASG: preast_var → preast_expr → preast_stm
| PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm
-| PREAST_STM_IF: ne_list (Prod preast_expr preast_decl) → option preast_decl → preast_stm
+| PREAST_STM_IF: ne_list (ProdT preast_expr preast_decl) → option preast_decl → preast_stm
(* dichiarazioni *)
with preast_decl : Type ≝
(* -------------------------- *)
(* programma *)
-inductive preast_root : Type ≝
+ninductive preast_root : Type ≝
PREAST_ROOT: preast_decl → preast_root.
(* -------------------------- *)
(* programma vuoto *)
-definition empty_preast_prog ≝ PREAST_ROOT (PREAST_NO_DECL (nil ?)).
+ndefinition empty_preast_prog ≝ PREAST_ROOT (PREAST_NO_DECL (nil ?)).