Functor Typed_ast.Exps_in_context

module Exps_in_context: 
functor (C : Exp_context) -> sig .. end

val exp_subst : Types.t Types.TNfmap.t * Typed_ast.exp_subst Typed_ast.Nfmap.t ->
       Typed_ast.exp -> Typed_ast.exp

val push_subst : Types.t Types.TNfmap.t * Typed_ast.exp_subst Typed_ast.Nfmap.t ->
       Typed_ast.pat list -> Typed_ast.exp -> Typed_ast.pat list * Typed_ast.exp

val exp_to_term : Typed_ast.exp -> Typed_ast.exp_aux

val exp_to_free : Typed_ast.exp -> Types.t Typed_ast.Nfmap.t

val type_eq : Ast.l -> string -> Types.t -> Types.t -> unit

val mk_lnumeral : Ast.l -> Typed_ast.lskips -> int -> Types.t option -> Typed_ast.lit

val mk_lnum : Ast.l -> Typed_ast.lskips -> int -> Types.t -> Typed_ast.lit

val mk_lbool : Ast.l -> Typed_ast.lskips -> bool -> Types.t option -> Typed_ast.lit

val mk_lbit : Ast.l -> Typed_ast.lskips -> int -> Types.t option -> Typed_ast.lit

val mk_lundef : Ast.l -> Typed_ast.lskips -> string -> Types.t -> Typed_ast.lit

val mk_lstring : Ast.l -> Typed_ast.lskips -> string -> Types.t option -> Typed_ast.lit

val mk_twild : Ast.l -> Typed_ast.lskips -> Types.t -> Types.src_t

val mk_tvar : Ast.l -> Typed_ast.lskips -> Tyvar.t -> Types.t -> Types.src_t

val mk_tfn : Ast.l ->
       Types.src_t ->
       Typed_ast.lskips -> Types.src_t -> Types.t option -> Types.src_t

val mk_ttup : Ast.l ->
       Types.src_t Typed_ast.lskips_seplist -> Types.t option -> Types.src_t

val mk_tapp : Ast.l -> Path.t Types.id -> Types.src_t list -> Types.t option -> Types.src_t

val mk_tparen : Ast.l ->
       Typed_ast.lskips ->
       Types.src_t -> Typed_ast.lskips -> Types.t option -> Types.src_t

val mk_pwild : Ast.l -> Typed_ast.lskips -> Types.t -> Typed_ast.pat

val mk_pas : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.pat ->
       Typed_ast.lskips ->
       Typed_ast.name_l -> Typed_ast.lskips -> Types.t option -> Typed_ast.pat

val mk_ptyp : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.pat ->
       Typed_ast.lskips ->
       Types.src_t -> Typed_ast.lskips -> Types.t option -> Typed_ast.pat

val mk_pvar : Ast.l -> Name.lskips_t -> Types.t -> Typed_ast.pat

val mk_pconst : Ast.l ->
       Typed_ast.const_descr_ref Types.id ->
       Typed_ast.pat list -> Types.t option -> Typed_ast.pat

val mk_pbackend : Ast.l ->
       Typed_ast.lskips ->
       Ident.t -> Types.t -> Typed_ast.pat list -> Types.t option -> Typed_ast.pat

val mk_precord : Ast.l ->
       Typed_ast.lskips ->
       (Typed_ast.const_descr_ref Types.id * Typed_ast.lskips * Typed_ast.pat)
       Typed_ast.lskips_seplist ->
       Typed_ast.lskips -> Types.t option -> Typed_ast.pat

val mk_ptup : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.pat Typed_ast.lskips_seplist ->
       Typed_ast.lskips -> Types.t option -> Typed_ast.pat

val mk_plist : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.pat Typed_ast.lskips_seplist ->
       Typed_ast.lskips -> Types.t -> Typed_ast.pat

val mk_pvector : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.pat Typed_ast.lskips_seplist ->
       Typed_ast.lskips -> Types.t -> Typed_ast.pat

val mk_pvectorc : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.pat list -> Typed_ast.lskips -> Types.t -> Typed_ast.pat

val mk_pparen : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.pat -> Typed_ast.lskips -> Types.t option -> Typed_ast.pat

val mk_pcons : Ast.l ->
       Typed_ast.pat ->
       Typed_ast.lskips -> Typed_ast.pat -> Types.t option -> Typed_ast.pat

val mk_pnum_add : Ast.l ->
       Typed_ast.name_l ->
       Typed_ast.lskips ->
       Typed_ast.lskips -> int -> Types.t option -> Typed_ast.pat

val mk_plit : Ast.l -> Typed_ast.lit -> Types.t option -> Typed_ast.pat

val mk_pvar_annot : Ast.l -> Name.lskips_t -> Types.src_t -> Types.t option -> Typed_ast.pat

val mk_var : Ast.l -> Name.lskips_t -> Types.t -> Typed_ast.exp

val mk_nvar_e : Ast.l -> Typed_ast.lskips -> Nvar.t -> Types.t -> Typed_ast.exp

val mk_backend : Ast.l -> Typed_ast.lskips -> Ident.t -> Types.t -> Typed_ast.exp

val mk_const : Ast.l ->
       Typed_ast.const_descr_ref Types.id -> Types.t option -> Typed_ast.exp

val mk_fun : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.pat list ->
       Typed_ast.lskips -> Typed_ast.exp -> Types.t option -> Typed_ast.exp

val mk_function : Ast.l ->
       Typed_ast.lskips ->
       (Typed_ast.pat * Typed_ast.lskips * Typed_ast.exp * Ast.l)
       Typed_ast.lskips_seplist ->
       Typed_ast.lskips -> Types.t option -> Typed_ast.exp

val mk_app : Ast.l -> Typed_ast.exp -> Typed_ast.exp -> Types.t option -> Typed_ast.exp

val mk_infix : Ast.l ->
       Typed_ast.exp ->
       Typed_ast.exp -> Typed_ast.exp -> Types.t option -> Typed_ast.exp

val mk_record : Ast.l ->
       Typed_ast.lskips ->
       (Typed_ast.const_descr_ref Types.id * Typed_ast.lskips * Typed_ast.exp *
        Ast.l)
       Typed_ast.lskips_seplist ->
       Typed_ast.lskips -> Types.t option -> Typed_ast.exp

val mk_recup : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.exp ->
       Typed_ast.lskips ->
       (Typed_ast.const_descr_ref Types.id * Typed_ast.lskips * Typed_ast.exp *
        Ast.l)
       Typed_ast.lskips_seplist ->
       Typed_ast.lskips -> Types.t option -> Typed_ast.exp

val mk_field : Ast.l ->
       Typed_ast.exp ->
       Typed_ast.lskips ->
       Typed_ast.const_descr_ref Types.id -> Types.t option -> Typed_ast.exp

val mk_case : bool ->
       Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.exp ->
       Typed_ast.lskips ->
       (Typed_ast.pat * Typed_ast.lskips * Typed_ast.exp * Ast.l)
       Typed_ast.lskips_seplist ->
       Typed_ast.lskips -> Types.t option -> Typed_ast.exp

val mk_typed : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.exp ->
       Typed_ast.lskips ->
       Types.src_t -> Typed_ast.lskips -> Types.t option -> Typed_ast.exp

val mk_let_val : Ast.l ->
       Typed_ast.pat ->
       (Typed_ast.lskips * Types.src_t) option ->
       Typed_ast.lskips -> Typed_ast.exp -> Typed_ast.letbind

val mk_let_fun : Ast.l ->
       Typed_ast.name_lskips_annot ->
       Typed_ast.pat list ->
       (Typed_ast.lskips * Types.src_t) option ->
       Typed_ast.lskips -> Typed_ast.exp -> Typed_ast.letbind

val mk_let : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.letbind ->
       Typed_ast.lskips -> Typed_ast.exp -> Types.t option -> Typed_ast.exp

val mk_tup : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.exp Typed_ast.lskips_seplist ->
       Typed_ast.lskips -> Types.t option -> Typed_ast.exp

val mk_list : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.exp Typed_ast.lskips_seplist ->
       Typed_ast.lskips -> Types.t -> Typed_ast.exp

val mk_vector : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.exp Typed_ast.lskips_seplist ->
       Typed_ast.lskips -> Types.t -> Typed_ast.exp

val mk_vaccess : Ast.l ->
       Typed_ast.exp ->
       Typed_ast.lskips ->
       Types.src_nexp -> Typed_ast.lskips -> Types.t -> Typed_ast.exp

val mk_vaccessr : Ast.l ->
       Typed_ast.exp ->
       Typed_ast.lskips ->
       Types.src_nexp ->
       Typed_ast.lskips ->
       Types.src_nexp -> Typed_ast.lskips -> Types.t -> Typed_ast.exp

val mk_paren : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.exp -> Typed_ast.lskips -> Types.t option -> Typed_ast.exp

val mk_begin : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.exp -> Typed_ast.lskips -> Types.t option -> Typed_ast.exp

val mk_if : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.exp ->
       Typed_ast.lskips ->
       Typed_ast.exp ->
       Typed_ast.lskips -> Typed_ast.exp -> Types.t option -> Typed_ast.exp

val mk_lit : Ast.l -> Typed_ast.lit -> Types.t option -> Typed_ast.exp

val mk_set : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.exp Typed_ast.lskips_seplist ->
       Typed_ast.lskips -> Types.t -> Typed_ast.exp

val mk_setcomp : Ast.l ->
       Typed_ast.lskips ->
       Typed_ast.exp ->
       Typed_ast.lskips ->
       Typed_ast.exp ->
       Typed_ast.lskips -> Typed_ast.NameSet.t -> Types.t option -> Typed_ast.exp

val mk_comp_binding : Ast.l ->
       bool ->
       Typed_ast.lskips ->
       Typed_ast.exp ->
       Typed_ast.lskips ->
       Typed_ast.lskips ->
       Typed_ast.quant_binding list ->
       Typed_ast.lskips ->
       Typed_ast.exp -> Typed_ast.lskips -> Types.t option -> Typed_ast.exp

val mk_quant : Ast.l ->
       Ast.q ->
       Typed_ast.quant_binding list ->
       Typed_ast.lskips -> Typed_ast.exp -> Types.t option -> Typed_ast.exp

val mk_do : Ast.l ->
       Typed_ast.lskips ->
       Path.t Types.id ->
       Typed_ast.do_line list ->
       Typed_ast.lskips ->
       Typed_ast.exp ->
       Typed_ast.lskips ->
       Types.t * Typed_ast.bind_tyargs_order -> Types.t option -> Typed_ast.exp

val t_to_src_t : Types.t -> Types.src_t

val pat_subst : Types.t Types.TNfmap.t * Name.t Typed_ast.Nfmap.t ->
       Typed_ast.pat -> Typed_ast.pat