Module UA.M

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