(* SUCCESSIONE APPIATITA DI ASSEGNAMENTI SU FLATENV *)
(* ************************************************ *)
+inductive jumpNLabel : Type ≝
+ N_LABEL: nat → jumpNLabel.
+
inductive jumpLabel : Type ≝
- BEGIN_LABEL: jumpLabel
-| N_LABEL: nat → jumpLabel
-| END_LABEL: jumpLabel.
+ LABEL_N: jumpNLabel → jumpLabel
+| LABEL_END: jumpLabel.
(*
L1 := goto L1
(* LABEL + [ init/assegnamenti ] + if(EXPR) then { goto LABEL; } else { goto LABEL; } *)
inductive linearfe_elem (e:aux_flatEnv_type) : Type ≝
- LINEARFE_ELEM: jumpLabel → list (linearfe_stm e) → jumpBlock e → linearfe_elem e.
+ LINEARFE_ELEM: jumpNLabel → list (linearfe_stm e) → jumpBlock e → linearfe_elem e.
(* -------------------------- *)