Module M.Make0

Parameters

module Span : sig ... end

Signature

val expr_If : typ:Hax_engine__Ast.Make(InputLanguage).ty -> cond:Hax_engine__Ast.Make(InputLanguage).expr -> then_:Hax_engine__Ast.Make(InputLanguage).expr -> else_:Hax_engine__Ast.Make(InputLanguage).expr Hax_engine.Prelude.option -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_App : typ:Hax_engine__Ast.Make(InputLanguage).ty -> f:Hax_engine__Ast.Make(InputLanguage).expr -> args:Hax_engine__Ast.Make(InputLanguage).expr Hax_engine.Prelude.list -> generic_args: Hax_engine__Ast.Make(InputLanguage).generic_value Hax_engine.Prelude.list -> bounds_impls: Hax_engine__Ast.Make(InputLanguage).impl_expr Hax_engine.Prelude.list -> trait: (Hax_engine__Ast.Make(InputLanguage).impl_expr * Hax_engine__Ast.Make(InputLanguage).generic_value Hax_engine.Prelude.list) Hax_engine.Prelude.option -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_Literal : typ:Hax_engine__Ast.Make(InputLanguage).ty -> Hax_engine.Ast.literal -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_Array : typ:Hax_engine__Ast.Make(InputLanguage).ty -> Hax_engine__Ast.Make(InputLanguage).expr Hax_engine.Prelude.list -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_Construct : typ:Hax_engine__Ast.Make(InputLanguage).ty -> constructor:Hax_engine.Ast.global_ident -> is_record:Hax_engine.Prelude.bool -> is_struct:Hax_engine.Prelude.bool -> fields: (Hax_engine.Ast.global_ident * Hax_engine__Ast.Make(InputLanguage).expr) Hax_engine.Prelude.list -> base: (Hax_engine__Ast.Make(InputLanguage).expr * InputLanguage.construct_base) Hax_engine.Prelude.option -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_Match : typ:Hax_engine__Ast.Make(InputLanguage).ty -> scrutinee:Hax_engine__Ast.Make(InputLanguage).expr -> arms:Hax_engine__Ast.Make(InputLanguage).arm Hax_engine.Prelude.list -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_Let : typ:Hax_engine__Ast.Make(InputLanguage).ty -> monadic: (Hax_engine__Ast.Make(InputLanguage).supported_monads * InputLanguage.monadic_binding) Hax_engine.Prelude.option -> lhs:Hax_engine__Ast.Make(InputLanguage).pat -> rhs:Hax_engine__Ast.Make(InputLanguage).expr -> body:Hax_engine__Ast.Make(InputLanguage).expr -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_Block : typ:Hax_engine__Ast.Make(InputLanguage).ty -> inner_e:Hax_engine__Ast.Make(InputLanguage).expr -> safety_mode:Hax_engine__Ast.Make(InputLanguage).safety_kind -> witness:InputLanguage.block -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_LocalVar : typ:Hax_engine__Ast.Make(InputLanguage).ty -> Hax_engine.Ast.local_ident -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_GlobalVar : typ:Hax_engine__Ast.Make(InputLanguage).ty -> Hax_engine.Ast.global_ident -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_Ascription : typ:Hax_engine__Ast.Make(InputLanguage).ty -> inner_e:Hax_engine__Ast.Make(InputLanguage).expr -> inner_typ:Hax_engine__Ast.Make(InputLanguage).ty -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_MacroInvokation : typ:Hax_engine__Ast.Make(InputLanguage).ty -> macro:Hax_engine.Ast.global_ident -> args:Hax_engine.Prelude.string -> witness:InputLanguage.macro -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_Assign : typ:Hax_engine__Ast.Make(InputLanguage).ty -> lhs:Hax_engine__Ast.Make(InputLanguage).lhs -> inner_e:Hax_engine__Ast.Make(InputLanguage).expr -> witness:InputLanguage.mutable_variable -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_Loop : typ:Hax_engine__Ast.Make(InputLanguage).ty -> body:Hax_engine__Ast.Make(InputLanguage).expr -> kind:Hax_engine__Ast.Make(InputLanguage).loop_kind -> state: Hax_engine__Ast.Make(InputLanguage).loop_state Hax_engine.Prelude.option -> control_flow: (Hax_engine__Ast.Make(InputLanguage).cf_kind * InputLanguage.fold_like_loop) Hax_engine.Prelude.option -> label:Hax_engine.Prelude.string Hax_engine.Prelude.option -> witness:InputLanguage.loop -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_Break : typ:Hax_engine__Ast.Make(InputLanguage).ty -> inner_e:Hax_engine__Ast.Make(InputLanguage).expr -> acc: (Hax_engine__Ast.Make(InputLanguage).expr * InputLanguage.state_passing_loop) Hax_engine.Prelude.option -> label:Hax_engine.Prelude.string Hax_engine.Prelude.option -> witness:(InputLanguage.break * InputLanguage.loop) -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_Return : typ:Hax_engine__Ast.Make(InputLanguage).ty -> inner_e:Hax_engine__Ast.Make(InputLanguage).expr -> witness:InputLanguage.early_exit -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_QuestionMark : typ:Hax_engine__Ast.Make(InputLanguage).ty -> inner_e:Hax_engine__Ast.Make(InputLanguage).expr -> return_typ:Hax_engine__Ast.Make(InputLanguage).ty -> witness:InputLanguage.question_mark -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_Continue : typ:Hax_engine__Ast.Make(InputLanguage).ty -> acc: (Hax_engine__Ast.Make(InputLanguage).expr * InputLanguage.state_passing_loop) Hax_engine.Prelude.option -> label:Hax_engine.Prelude.string Hax_engine.Prelude.option -> witness:(InputLanguage.continue * InputLanguage.loop) -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_Borrow : typ:Hax_engine__Ast.Make(InputLanguage).ty -> kind:Hax_engine__Ast.Make(InputLanguage).borrow_kind -> inner_e:Hax_engine__Ast.Make(InputLanguage).expr -> witness:InputLanguage.reference -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_AddressOf : typ:Hax_engine__Ast.Make(InputLanguage).ty -> mut:InputLanguage.mutable_pointer Hax_engine.Ast.mutability -> inner_e:Hax_engine__Ast.Make(InputLanguage).expr -> witness:InputLanguage.raw_pointer -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_Closure : typ:Hax_engine__Ast.Make(InputLanguage).ty -> params:Hax_engine__Ast.Make(InputLanguage).pat Hax_engine.Prelude.list -> body:Hax_engine__Ast.Make(InputLanguage).expr -> captures:Hax_engine__Ast.Make(InputLanguage).expr Hax_engine.Prelude.list -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_EffectAction : typ:Hax_engine__Ast.Make(InputLanguage).ty -> action:InputLanguage.monadic_action -> argument:Hax_engine__Ast.Make(InputLanguage).expr -> Hax_engine__Ast.Make(InputLanguage).expr
val expr_Quote : typ:Hax_engine__Ast.Make(InputLanguage).ty -> Hax_engine__Ast.Make(InputLanguage).quote -> Hax_engine__Ast.Make(InputLanguage).expr
val pat_PWild : typ:Hax_engine__Ast.Make(InputLanguage).ty -> Hax_engine__Ast.Make(InputLanguage).pat
val pat_PAscription : typ:Hax_engine__Ast.Make(InputLanguage).ty -> inner_typ:Hax_engine__Ast.Make(InputLanguage).ty -> typ_span:Hax_engine.Ast.span -> pat:Hax_engine__Ast.Make(InputLanguage).pat -> Hax_engine__Ast.Make(InputLanguage).pat
val pat_PConstruct : typ:Hax_engine__Ast.Make(InputLanguage).ty -> constructor:Hax_engine.Ast.global_ident -> is_record:Hax_engine.Prelude.bool -> is_struct:Hax_engine.Prelude.bool -> fields:Hax_engine__Ast.Make(InputLanguage).field_pat Hax_engine.Prelude.list -> Hax_engine__Ast.Make(InputLanguage).pat
val pat_POr : typ:Hax_engine__Ast.Make(InputLanguage).ty -> subpats:Hax_engine__Ast.Make(InputLanguage).pat Hax_engine.Prelude.list -> Hax_engine__Ast.Make(InputLanguage).pat
val pat_PArray : typ:Hax_engine__Ast.Make(InputLanguage).ty -> args:Hax_engine__Ast.Make(InputLanguage).pat Hax_engine.Prelude.list -> Hax_engine__Ast.Make(InputLanguage).pat
val pat_PDeref : typ:Hax_engine__Ast.Make(InputLanguage).ty -> subpat:Hax_engine__Ast.Make(InputLanguage).pat -> witness:InputLanguage.reference -> Hax_engine__Ast.Make(InputLanguage).pat
val pat_PConstant : typ:Hax_engine__Ast.Make(InputLanguage).ty -> lit:Hax_engine.Ast.literal -> Hax_engine__Ast.Make(InputLanguage).pat
val item_Fn : ident:Hax_engine.Ast.concrete_ident -> attrs:Hax_engine.Ast.attrs -> name:Hax_engine.Ast.concrete_ident -> generics:Hax_engine__Ast.Make(InputLanguage).generics -> body:Hax_engine__Ast.Make(InputLanguage).expr -> params:Hax_engine__Ast.Make(InputLanguage).param Hax_engine.Prelude.list -> safety:Hax_engine__Ast.Make(InputLanguage).safety_kind -> Hax_engine__Ast.Make(InputLanguage).item
val item_TyAlias : ident:Hax_engine.Ast.concrete_ident -> attrs:Hax_engine.Ast.attrs -> name:Hax_engine.Ast.concrete_ident -> generics:Hax_engine__Ast.Make(InputLanguage).generics -> ty:Hax_engine__Ast.Make(InputLanguage).ty -> Hax_engine__Ast.Make(InputLanguage).item
val item_Type : ident:Hax_engine.Ast.concrete_ident -> attrs:Hax_engine.Ast.attrs -> name:Hax_engine.Ast.concrete_ident -> generics:Hax_engine__Ast.Make(InputLanguage).generics -> variants:Hax_engine__Ast.Make(InputLanguage).variant Hax_engine.Prelude.list -> is_struct:Hax_engine.Prelude.bool -> Hax_engine__Ast.Make(InputLanguage).item
val item_IMacroInvokation : ident:Hax_engine.Ast.concrete_ident -> attrs:Hax_engine.Ast.attrs -> macro:Hax_engine.Ast.concrete_ident -> argument:Hax_engine.Prelude.string -> inner_span:Hax_engine.Ast.span -> witness:InputLanguage.macro -> Hax_engine__Ast.Make(InputLanguage).item
val item_Trait : ident:Hax_engine.Ast.concrete_ident -> attrs:Hax_engine.Ast.attrs -> name:Hax_engine.Ast.concrete_ident -> generics:Hax_engine__Ast.Make(InputLanguage).generics -> items:Hax_engine__Ast.Make(InputLanguage).trait_item Hax_engine.Prelude.list -> safety:Hax_engine__Ast.Make(InputLanguage).safety_kind -> Hax_engine__Ast.Make(InputLanguage).item
val item_Impl : ident:Hax_engine.Ast.concrete_ident -> attrs:Hax_engine.Ast.attrs -> generics:Hax_engine__Ast.Make(InputLanguage).generics -> self_ty:Hax_engine__Ast.Make(InputLanguage).ty -> of_trait: (Hax_engine.Ast.concrete_ident * Hax_engine__Ast.Make(InputLanguage).generic_value Hax_engine.Prelude.list) -> items:Hax_engine__Ast.Make(InputLanguage).impl_item Hax_engine.Prelude.list -> parent_bounds: (Hax_engine__Ast.Make(InputLanguage).impl_expr * Hax_engine__Ast.Make(InputLanguage).impl_ident) Hax_engine.Prelude.list -> safety:Hax_engine__Ast.Make(InputLanguage).safety_kind -> Hax_engine__Ast.Make(InputLanguage).item
val item_Alias : ident:Hax_engine.Ast.concrete_ident -> attrs:Hax_engine.Ast.attrs -> name:Hax_engine.Ast.concrete_ident -> item:Hax_engine.Ast.concrete_ident -> Hax_engine__Ast.Make(InputLanguage).item
val item_Quote : ident:Hax_engine.Ast.concrete_ident -> attrs:Hax_engine.Ast.attrs -> quote:Hax_engine__Ast.Make(InputLanguage).quote -> origin:Hax_engine.Ast.item_quote_origin -> Hax_engine__Ast.Make(InputLanguage).item
val item_HaxError : ident:Hax_engine.Ast.concrete_ident -> attrs:Hax_engine.Ast.attrs -> Hax_engine.Prelude.string -> Hax_engine__Ast.Make(InputLanguage).item
val item_NotImplementedYet : ident:Hax_engine.Ast.concrete_ident -> attrs:Hax_engine.Ast.attrs -> Hax_engine__Ast.Make(InputLanguage).item
val guard_IfLet : lhs:Hax_engine__Ast.Make(InputLanguage).pat -> rhs:Hax_engine__Ast.Make(InputLanguage).expr -> witness:InputLanguage.match_guard -> Hax_engine__Ast.Make(InputLanguage).guard
val trait_item_TIType : ti_span:Hax_engine.Ast.span -> ti_generics:Hax_engine__Ast.Make(InputLanguage).generics -> ti_ident:Hax_engine.Ast.concrete_ident -> ti_attrs:Hax_engine.Ast.attrs -> Hax_engine__Ast.Make(InputLanguage).impl_ident Hax_engine.Prelude.list -> Hax_engine__Ast.Make(InputLanguage).trait_item
val trait_item_TIFn : ti_span:Hax_engine.Ast.span -> ti_generics:Hax_engine__Ast.Make(InputLanguage).generics -> ti_ident:Hax_engine.Ast.concrete_ident -> ti_attrs:Hax_engine.Ast.attrs -> Hax_engine__Ast.Make(InputLanguage).ty -> Hax_engine__Ast.Make(InputLanguage).trait_item
val trait_item_TIDefault : ti_span:Hax_engine.Ast.span -> ti_generics:Hax_engine__Ast.Make(InputLanguage).generics -> ti_ident:Hax_engine.Ast.concrete_ident -> ti_attrs:Hax_engine.Ast.attrs -> params:Hax_engine__Ast.Make(InputLanguage).param Hax_engine.Prelude.list -> body:Hax_engine__Ast.Make(InputLanguage).expr -> witness:InputLanguage.trait_item_default -> Hax_engine__Ast.Make(InputLanguage).trait_item
val impl_expr_Self : goal:Hax_engine__Ast.Make(InputLanguage).trait_goal -> Hax_engine__Ast.Make(InputLanguage).impl_expr
val impl_expr_Concrete : goal:Hax_engine__Ast.Make(InputLanguage).trait_goal -> Hax_engine__Ast.Make(InputLanguage).trait_goal -> Hax_engine__Ast.Make(InputLanguage).impl_expr
val impl_expr_LocalBound : goal:Hax_engine__Ast.Make(InputLanguage).trait_goal -> id:Hax_engine.Prelude.string -> Hax_engine__Ast.Make(InputLanguage).impl_expr
val impl_expr_Parent : goal:Hax_engine__Ast.Make(InputLanguage).trait_goal -> impl:Hax_engine__Ast.Make(InputLanguage).impl_expr -> ident:Hax_engine__Ast.Make(InputLanguage).impl_ident -> Hax_engine__Ast.Make(InputLanguage).impl_expr
val impl_expr_Projection : goal:Hax_engine__Ast.Make(InputLanguage).trait_goal -> impl:Hax_engine__Ast.Make(InputLanguage).impl_expr -> item:Hax_engine.Ast.concrete_ident -> ident:Hax_engine__Ast.Make(InputLanguage).impl_ident -> Hax_engine__Ast.Make(InputLanguage).impl_expr
val impl_expr_ImplApp : goal:Hax_engine__Ast.Make(InputLanguage).trait_goal -> impl:Hax_engine__Ast.Make(InputLanguage).impl_expr -> args:Hax_engine__Ast.Make(InputLanguage).impl_expr Hax_engine.Prelude.list -> Hax_engine__Ast.Make(InputLanguage).impl_expr
val impl_expr_Dyn : goal:Hax_engine__Ast.Make(InputLanguage).trait_goal -> Hax_engine__Ast.Make(InputLanguage).impl_expr
val impl_expr_Builtin : goal:Hax_engine__Ast.Make(InputLanguage).trait_goal -> Hax_engine__Ast.Make(InputLanguage).trait_goal -> Hax_engine__Ast.Make(InputLanguage).impl_expr
val ty_tuple_or_id : AST.ty Hax_engine.Prelude.list -> AST.ty
val ty_cf : continue_type:AST.ty -> break_type:AST.ty -> AST.ty
val ty_cf_return : acc_type:AST.ty -> break_type:AST.ty -> return_type:AST.ty Hax_engine.Prelude.option -> AST.ty
val pat_PBinding : typ:Hax_engine__Ast.Make(InputLanguage).ty -> mut:InputLanguage.mutable_variable Hax_engine.Ast.mutability -> mode:Hax_engine__Ast.Make(InputLanguage).binding_mode -> var:Hax_engine.Ast.local_ident -> subpat: (Hax_engine__Ast.Make(InputLanguage).pat * InputLanguage.as_pattern) Hax_engine.Prelude.option -> Hax_engine__Ast.Make(InputLanguage).pat
val expr_unit : Hax_engine__Ast.Make(InputLanguage).expr
val pat_Constructor_CF : typ:AST.ty -> [ `Break | `Continue ] -> AST.pat -> AST.pat
val expr'_Constructor_CF : break_type:AST.ty -> ?continue_type:AST.ty -> [ `Break | `Continue ] -> AST.expr -> AST.expr
val expr_Constructor_CF : break_type:AST.ty Hax_engine.Prelude.option -> return_type:AST.ty Hax_engine.Prelude.option -> acc:AST.expr -> ?e:AST.expr -> [ `Break | `Continue | `Return ] -> AST.expr