- ast_expr e t → ast_base_expr e.
-
-(* -------------------------- *)
-
-(* espressioni destre di assegnamento *)
-inductive ast_right_expr (e:aux_env_type) : ast_type → Type ≝
- AST_RIGHT_EXPR_BASE: ∀t:ast_base_type.
- ast_expr e t → ast_right_expr e (AST_TYPE_BASE t)
-| AST_RIGHT_EXPR_VAR: ∀b:bool.∀t:ast_type.
- ast_var e b t → ast_right_expr e t.