-definition preast_to_ast_right_expr : preast_expr → Πe.option (Σt:ast_type.ast_right_expr e t) ≝
-λpreast:preast_expr.λe:aux_env_type.match preast with
- (* NB: PREAST_EXPR_ID viene sempre tradotto come AST_RIGHT_EXPR_VAR *)
- [ PREAST_EXPR_ID var ⇒
- opt_map ?? (preast_to_ast_var var e)
- (λsigmaRes:(Σb:bool.(Σt:ast_type.ast_var e b t)).
- Some (Σt:ast_type.ast_right_expr e t) ≪?,(AST_RIGHT_EXPR_VAR e ?? (sigmaSnd ?? (sigmaSnd ?? sigmaRes)))≫)
-
- | _ ⇒
- opt_map ?? (preast_to_ast_expr preast e)
- (λsigmaRes:(Σt:ast_base_type.ast_expr e t).
- Some (Σt:ast_type.ast_right_expr e t) ≪ (AST_TYPE_BASE ?),(AST_RIGHT_EXPR_BASE e ? (sigmaSnd ?? sigmaRes))≫)
- ].
-