Module U.D

type expr_If = {
  1. cond : Hax_engine__Ast.Make(InputLanguage).expr;
  2. then_ : Hax_engine__Ast.Make(InputLanguage).expr;
  3. else_ : Hax_engine__Ast.Make(InputLanguage).expr Hax_engine.Prelude.option;
}
val expr_If : Hax_engine__Ast.Make(InputLanguage).expr -> expr_If Hax_engine.Prelude.option
type expr_App = {
  1. f : Hax_engine__Ast.Make(InputLanguage).expr;
  2. args : Hax_engine__Ast.Make(InputLanguage).expr Hax_engine.Prelude.list;
  3. generic_args : Hax_engine__Ast.Make(InputLanguage).generic_value Hax_engine.Prelude.list;
  4. bounds_impls : Hax_engine__Ast.Make(InputLanguage).impl_expr Hax_engine.Prelude.list;
  5. trait : (Hax_engine__Ast.Make(InputLanguage).impl_expr * Hax_engine__Ast.Make(InputLanguage).generic_value Hax_engine.Prelude.list) Hax_engine.Prelude.option;
}
val expr_App : Hax_engine__Ast.Make(InputLanguage).expr -> expr_App Hax_engine.Prelude.option
type expr_Literal = Hax_engine.Ast.literal
val expr_Literal : Hax_engine__Ast.Make(InputLanguage).expr -> expr_Literal Hax_engine.Prelude.option
type expr_Array = Hax_engine__Ast.Make(InputLanguage).expr Hax_engine.Prelude.list
val expr_Array : Hax_engine__Ast.Make(InputLanguage).expr -> expr_Array Hax_engine.Prelude.option
type expr_Construct = {
  1. constructor : Hax_engine.Ast.global_ident;
  2. is_record : Hax_engine.Prelude.bool;
  3. is_struct : Hax_engine.Prelude.bool;
  4. fields : (Hax_engine.Ast.global_ident * Hax_engine__Ast.Make(InputLanguage).expr) Hax_engine.Prelude.list;
  5. base : (Hax_engine__Ast.Make(InputLanguage).expr * InputLanguage.construct_base) Hax_engine.Prelude.option;
}
val expr_Construct : Hax_engine__Ast.Make(InputLanguage).expr -> expr_Construct Hax_engine.Prelude.option
type expr_Match = {
  1. scrutinee : Hax_engine__Ast.Make(InputLanguage).expr;
  2. arms : Hax_engine__Ast.Make(InputLanguage).arm Hax_engine.Prelude.list;
}
val expr_Match : Hax_engine__Ast.Make(InputLanguage).expr -> expr_Match Hax_engine.Prelude.option
type expr_Let = {
  1. monadic : (Hax_engine__Ast.Make(InputLanguage).supported_monads * InputLanguage.monadic_binding) Hax_engine.Prelude.option;
  2. lhs : Hax_engine__Ast.Make(InputLanguage).pat;
  3. rhs : Hax_engine__Ast.Make(InputLanguage).expr;
  4. body : Hax_engine__Ast.Make(InputLanguage).expr;
}
val expr_Let : Hax_engine__Ast.Make(InputLanguage).expr -> expr_Let Hax_engine.Prelude.option
type expr_Block = {
  1. e : Hax_engine__Ast.Make(InputLanguage).expr;
  2. safety_mode : Hax_engine__Ast.Make(InputLanguage).safety_kind;
  3. witness : InputLanguage.block;
}
val expr_Block : Hax_engine__Ast.Make(InputLanguage).expr -> expr_Block Hax_engine.Prelude.option
type expr_LocalVar = Hax_engine.Ast.local_ident
val expr_LocalVar : Hax_engine__Ast.Make(InputLanguage).expr -> expr_LocalVar Hax_engine.Prelude.option
type expr_GlobalVar = Hax_engine.Ast.global_ident
val expr_GlobalVar : Hax_engine__Ast.Make(InputLanguage).expr -> expr_GlobalVar Hax_engine.Prelude.option
type expr_Ascription = {
  1. e : Hax_engine__Ast.Make(InputLanguage).expr;
  2. typ : Hax_engine__Ast.Make(InputLanguage).ty;
}
val expr_Ascription : Hax_engine__Ast.Make(InputLanguage).expr -> expr_Ascription Hax_engine.Prelude.option
type expr_MacroInvokation = {
  1. macro : Hax_engine.Ast.global_ident;
  2. args : Hax_engine.Prelude.string;
  3. witness : InputLanguage.macro;
}
val expr_MacroInvokation : Hax_engine__Ast.Make(InputLanguage).expr -> expr_MacroInvokation Hax_engine.Prelude.option
type expr_Assign = {
  1. lhs : Hax_engine__Ast.Make(InputLanguage).lhs;
  2. e : Hax_engine__Ast.Make(InputLanguage).expr;
  3. witness : InputLanguage.mutable_variable;
}
val expr_Assign : Hax_engine__Ast.Make(InputLanguage).expr -> expr_Assign Hax_engine.Prelude.option
type expr_Loop = {
  1. body : Hax_engine__Ast.Make(InputLanguage).expr;
  2. kind : Hax_engine__Ast.Make(InputLanguage).loop_kind;
  3. state : Hax_engine__Ast.Make(InputLanguage).loop_state Hax_engine.Prelude.option;
  4. control_flow : (Hax_engine__Ast.Make(InputLanguage).cf_kind * InputLanguage.fold_like_loop) Hax_engine.Prelude.option;
  5. label : Hax_engine.Prelude.string Hax_engine.Prelude.option;
  6. witness : InputLanguage.loop;
}
val expr_Loop : Hax_engine__Ast.Make(InputLanguage).expr -> expr_Loop Hax_engine.Prelude.option
type expr_Break = {
  1. e : Hax_engine__Ast.Make(InputLanguage).expr;
  2. acc : (Hax_engine__Ast.Make(InputLanguage).expr * InputLanguage.state_passing_loop) Hax_engine.Prelude.option;
  3. label : Hax_engine.Prelude.string Hax_engine.Prelude.option;
  4. witness : InputLanguage.break * InputLanguage.loop;
}
val expr_Break : Hax_engine__Ast.Make(InputLanguage).expr -> expr_Break Hax_engine.Prelude.option
type expr_Return = {
  1. e : Hax_engine__Ast.Make(InputLanguage).expr;
  2. witness : InputLanguage.early_exit;
}
val expr_Return : Hax_engine__Ast.Make(InputLanguage).expr -> expr_Return Hax_engine.Prelude.option
type expr_QuestionMark = {
  1. e : Hax_engine__Ast.Make(InputLanguage).expr;
  2. return_typ : Hax_engine__Ast.Make(InputLanguage).ty;
  3. witness : InputLanguage.question_mark;
}
val expr_QuestionMark : Hax_engine__Ast.Make(InputLanguage).expr -> expr_QuestionMark Hax_engine.Prelude.option
type expr_Continue = {
  1. acc : (Hax_engine__Ast.Make(InputLanguage).expr * InputLanguage.state_passing_loop) Hax_engine.Prelude.option;
  2. label : Hax_engine.Prelude.string Hax_engine.Prelude.option;
  3. witness : InputLanguage.continue * InputLanguage.loop;
}
val expr_Continue : Hax_engine__Ast.Make(InputLanguage).expr -> expr_Continue Hax_engine.Prelude.option
type expr_Borrow = {
  1. kind : Hax_engine__Ast.Make(InputLanguage).borrow_kind;
  2. e : Hax_engine__Ast.Make(InputLanguage).expr;
  3. witness : InputLanguage.reference;
}
val expr_Borrow : Hax_engine__Ast.Make(InputLanguage).expr -> expr_Borrow Hax_engine.Prelude.option
type expr_AddressOf = {
  1. mut : InputLanguage.mutable_pointer Hax_engine.Ast.mutability;
  2. e : Hax_engine__Ast.Make(InputLanguage).expr;
  3. witness : InputLanguage.raw_pointer;
}
val expr_AddressOf : Hax_engine__Ast.Make(InputLanguage).expr -> expr_AddressOf Hax_engine.Prelude.option
type expr_Closure = {
  1. params : Hax_engine__Ast.Make(InputLanguage).pat Hax_engine.Prelude.list;
  2. body : Hax_engine__Ast.Make(InputLanguage).expr;
  3. captures : Hax_engine__Ast.Make(InputLanguage).expr Hax_engine.Prelude.list;
}
val expr_Closure : Hax_engine__Ast.Make(InputLanguage).expr -> expr_Closure Hax_engine.Prelude.option
type expr_EffectAction = {
  1. action : InputLanguage.monadic_action;
  2. argument : Hax_engine__Ast.Make(InputLanguage).expr;
}
val expr_EffectAction : Hax_engine__Ast.Make(InputLanguage).expr -> expr_EffectAction Hax_engine.Prelude.option
type expr_Quote
val expr_Quote : Hax_engine__Ast.Make(InputLanguage).expr -> expr_Quote Hax_engine.Prelude.option
type pat_PWild = Hax_engine.Prelude.unit
val pat_PWild : Hax_engine__Ast.Make(InputLanguage).pat -> pat_PWild Hax_engine.Prelude.option
type pat_PAscription = {
  1. typ : Hax_engine__Ast.Make(InputLanguage).ty;
  2. typ_span : Hax_engine.Ast.span;
  3. pat : Hax_engine__Ast.Make(InputLanguage).pat;
}
val pat_PAscription : Hax_engine__Ast.Make(InputLanguage).pat -> pat_PAscription Hax_engine.Prelude.option
type pat_PConstruct = {
  1. constructor : Hax_engine.Ast.global_ident;
  2. is_record : Hax_engine.Prelude.bool;
  3. is_struct : Hax_engine.Prelude.bool;
  4. fields : Hax_engine__Ast.Make(InputLanguage).field_pat Hax_engine.Prelude.list;
}
val pat_PConstruct : Hax_engine__Ast.Make(InputLanguage).pat -> pat_PConstruct Hax_engine.Prelude.option
type pat_POr = {
  1. subpats : Hax_engine__Ast.Make(InputLanguage).pat Hax_engine.Prelude.list;
}
val pat_POr : Hax_engine__Ast.Make(InputLanguage).pat -> pat_POr Hax_engine.Prelude.option
type pat_PArray = {
  1. args : Hax_engine__Ast.Make(InputLanguage).pat Hax_engine.Prelude.list;
}
val pat_PArray : Hax_engine__Ast.Make(InputLanguage).pat -> pat_PArray Hax_engine.Prelude.option
type pat_PDeref = {
  1. subpat : Hax_engine__Ast.Make(InputLanguage).pat;
  2. witness : InputLanguage.reference;
}
val pat_PDeref : Hax_engine__Ast.Make(InputLanguage).pat -> pat_PDeref Hax_engine.Prelude.option
type pat_PConstant = {
  1. lit : Hax_engine.Ast.literal;
}
val pat_PConstant : Hax_engine__Ast.Make(InputLanguage).pat -> pat_PConstant Hax_engine.Prelude.option
type pat_PBinding = {
  1. mut : InputLanguage.mutable_variable Hax_engine.Ast.mutability;
  2. mode : Hax_engine__Ast.Make(InputLanguage).binding_mode;
  3. var : Hax_engine.Ast.local_ident;
  4. typ : Hax_engine__Ast.Make(InputLanguage).ty;
  5. subpat : (Hax_engine__Ast.Make(InputLanguage).pat * InputLanguage.as_pattern) Hax_engine.Prelude.option;
}
val pat_PBinding : Hax_engine__Ast.Make(InputLanguage).pat -> pat_PBinding Hax_engine.Prelude.option
type item_Fn = {
  1. name : Hax_engine.Ast.concrete_ident;
  2. generics : Hax_engine__Ast.Make(InputLanguage).generics;
  3. body : Hax_engine__Ast.Make(InputLanguage).expr;
  4. params : Hax_engine__Ast.Make(InputLanguage).param Hax_engine.Prelude.list;
  5. safety : Hax_engine__Ast.Make(InputLanguage).safety_kind;
}
val item_Fn : Hax_engine__Ast.Make(InputLanguage).item -> item_Fn Hax_engine.Prelude.option
type item_TyAlias = {
  1. name : Hax_engine.Ast.concrete_ident;
  2. generics : Hax_engine__Ast.Make(InputLanguage).generics;
  3. ty : Hax_engine__Ast.Make(InputLanguage).ty;
}
val item_TyAlias : Hax_engine__Ast.Make(InputLanguage).item -> item_TyAlias Hax_engine.Prelude.option
type item_Type = {
  1. name : Hax_engine.Ast.concrete_ident;
  2. generics : Hax_engine__Ast.Make(InputLanguage).generics;
  3. variants : Hax_engine__Ast.Make(InputLanguage).variant Hax_engine.Prelude.list;
  4. is_struct : Hax_engine.Prelude.bool;
}
val item_Type : Hax_engine__Ast.Make(InputLanguage).item -> item_Type Hax_engine.Prelude.option
type item_IMacroInvokation = {
  1. macro : Hax_engine.Ast.concrete_ident;
  2. argument : Hax_engine.Prelude.string;
  3. span : Hax_engine.Ast.span;
  4. witness : InputLanguage.macro;
}
val item_IMacroInvokation : Hax_engine__Ast.Make(InputLanguage).item -> item_IMacroInvokation Hax_engine.Prelude.option
type item_Trait = {
  1. name : Hax_engine.Ast.concrete_ident;
  2. generics : Hax_engine__Ast.Make(InputLanguage).generics;
  3. items : Hax_engine__Ast.Make(InputLanguage).trait_item Hax_engine.Prelude.list;
  4. safety : Hax_engine__Ast.Make(InputLanguage).safety_kind;
}
val item_Trait : Hax_engine__Ast.Make(InputLanguage).item -> item_Trait Hax_engine.Prelude.option
type item_Impl = {
  1. generics : Hax_engine__Ast.Make(InputLanguage).generics;
  2. self_ty : Hax_engine__Ast.Make(InputLanguage).ty;
  3. of_trait : Hax_engine.Ast.concrete_ident * Hax_engine__Ast.Make(InputLanguage).generic_value Hax_engine.Prelude.list;
  4. items : Hax_engine__Ast.Make(InputLanguage).impl_item Hax_engine.Prelude.list;
  5. parent_bounds : (Hax_engine__Ast.Make(InputLanguage).impl_expr * Hax_engine__Ast.Make(InputLanguage).impl_ident) Hax_engine.Prelude.list;
  6. safety : Hax_engine__Ast.Make(InputLanguage).safety_kind;
}
val item_Impl : Hax_engine__Ast.Make(InputLanguage).item -> item_Impl Hax_engine.Prelude.option
val item_Alias : Hax_engine__Ast.Make(InputLanguage).item -> item_Alias Hax_engine.Prelude.option
val item_Use : Hax_engine__Ast.Make(InputLanguage).item -> item_Use Hax_engine.Prelude.option
type item_Quote = {
  1. quote : Hax_engine__Ast.Make(InputLanguage).quote;
  2. origin : Hax_engine.Ast.item_quote_origin;
}
val item_Quote : Hax_engine__Ast.Make(InputLanguage).item -> item_Quote Hax_engine.Prelude.option
type item_HaxError = Hax_engine.Prelude.string
val item_HaxError : Hax_engine__Ast.Make(InputLanguage).item -> item_HaxError Hax_engine.Prelude.option
type item_NotImplementedYet = Hax_engine.Prelude.unit
val item_NotImplementedYet : Hax_engine__Ast.Make(InputLanguage).item -> item_NotImplementedYet Hax_engine.Prelude.option
type guard_IfLet = {
  1. lhs : Hax_engine__Ast.Make(InputLanguage).pat;
  2. rhs : Hax_engine__Ast.Make(InputLanguage).expr;
  3. witness : InputLanguage.match_guard;
}
val guard_IfLet : Hax_engine__Ast.Make(InputLanguage).guard -> guard_IfLet Hax_engine.Prelude.option
type trait_item_TIType = Hax_engine__Ast.Make(InputLanguage).impl_ident Hax_engine.Prelude.list
val trait_item_TIType : Hax_engine__Ast.Make(InputLanguage).trait_item -> trait_item_TIType Hax_engine.Prelude.option
type trait_item_TIFn
val trait_item_TIFn : Hax_engine__Ast.Make(InputLanguage).trait_item -> trait_item_TIFn Hax_engine.Prelude.option
type trait_item_TIDefault = {
  1. params : Hax_engine__Ast.Make(InputLanguage).param Hax_engine.Prelude.list;
  2. body : Hax_engine__Ast.Make(InputLanguage).expr;
  3. witness : InputLanguage.trait_item_default;
}
val trait_item_TIDefault : Hax_engine__Ast.Make(InputLanguage).trait_item -> trait_item_TIDefault Hax_engine.Prelude.option
type impl_expr_Self = Hax_engine.Prelude.unit
val impl_expr_Self : Hax_engine__Ast.Make(InputLanguage).impl_expr -> impl_expr_Self Hax_engine.Prelude.option
type impl_expr_Concrete
val impl_expr_Concrete : Hax_engine__Ast.Make(InputLanguage).impl_expr -> impl_expr_Concrete Hax_engine.Prelude.option
type impl_expr_LocalBound = {
  1. id : Hax_engine.Prelude.string;
}
val impl_expr_LocalBound : Hax_engine__Ast.Make(InputLanguage).impl_expr -> impl_expr_LocalBound Hax_engine.Prelude.option
type impl_expr_Parent = {
  1. impl : Hax_engine__Ast.Make(InputLanguage).impl_expr;
  2. ident : Hax_engine__Ast.Make(InputLanguage).impl_ident;
}
val impl_expr_Parent : Hax_engine__Ast.Make(InputLanguage).impl_expr -> impl_expr_Parent Hax_engine.Prelude.option
type impl_expr_Projection = {
  1. impl : Hax_engine__Ast.Make(InputLanguage).impl_expr;
  2. item : Hax_engine.Ast.concrete_ident;
  3. ident : Hax_engine__Ast.Make(InputLanguage).impl_ident;
}
val impl_expr_Projection : Hax_engine__Ast.Make(InputLanguage).impl_expr -> impl_expr_Projection Hax_engine.Prelude.option
type impl_expr_ImplApp = {
  1. impl : Hax_engine__Ast.Make(InputLanguage).impl_expr;
  2. args : Hax_engine__Ast.Make(InputLanguage).impl_expr Hax_engine.Prelude.list;
}
val impl_expr_ImplApp : Hax_engine__Ast.Make(InputLanguage).impl_expr -> impl_expr_ImplApp Hax_engine.Prelude.option
type impl_expr_Dyn = Hax_engine.Prelude.unit
val impl_expr_Dyn : Hax_engine__Ast.Make(InputLanguage).impl_expr -> impl_expr_Dyn Hax_engine.Prelude.option
type impl_expr_Builtin
val impl_expr_Builtin : Hax_engine__Ast.Make(InputLanguage).impl_expr -> impl_expr_Builtin Hax_engine.Prelude.option
val list_0 : 'a list -> unit option
val list_1 : 'a list -> 'a option
val list_2 : 'a list -> ('a * 'a) option
val list_3 : 'a list -> ('a * 'a * 'a) option
val list_4 : 'a list -> ('a * 'a * 'a * 'a) option
val list_5 : 'a list -> ('a * 'a * 'a * 'a * 'a) option