M (hax-engine.Fstar_backend.Attrs.U.M)

module AST : sig ... end

module type SPAN = sig ... end

val expr_If : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  typ:Hax_engine__Ast.Make(InputLanguage).ty ->
  Hax_engine.Ast.literal ->
  Hax_engine__Ast.Make(InputLanguage).expr

val expr_Array : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  typ:Hax_engine__Ast.Make(InputLanguage).ty ->
  Hax_engine.Ast.local_ident ->
  Hax_engine__Ast.Make(InputLanguage).expr

val expr_GlobalVar : 
  span:Hax_engine.Ast.span ->
  typ:Hax_engine__Ast.Make(InputLanguage).ty ->
  Hax_engine.Ast.global_ident ->
  Hax_engine__Ast.Make(InputLanguage).expr

val expr_Ascription : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  typ:Hax_engine__Ast.Make(InputLanguage).ty ->
  Hax_engine__Ast.Make(InputLanguage).quote ->
  Hax_engine__Ast.Make(InputLanguage).expr

val pat_PWild : 
  span:Hax_engine.Ast.span ->
  typ:Hax_engine__Ast.Make(InputLanguage).ty ->
  Hax_engine__Ast.Make(InputLanguage).pat

val pat_PAscription : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  typ:Hax_engine__Ast.Make(InputLanguage).ty ->
  lit:Hax_engine.Ast.literal ->
  Hax_engine__Ast.Make(InputLanguage).pat

val item_Fn : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  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_Use : 
  span:Hax_engine.Ast.span ->
  ident:Hax_engine.Ast.concrete_ident ->
  attrs:Hax_engine.Ast.attrs ->
  path:Hax_engine.Prelude.string Hax_engine.Prelude.list ->
  is_external:Hax_engine.Prelude.bool ->
  rename:Hax_engine.Prelude.string Hax_engine.Prelude.option ->
  Hax_engine__Ast.Make(InputLanguage).item

val item_Quote : 
  span:Hax_engine.Ast.span ->
  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 : 
  span:Hax_engine.Ast.span ->
  ident:Hax_engine.Ast.concrete_ident ->
  attrs:Hax_engine.Ast.attrs ->
  Hax_engine.Prelude.string ->
  Hax_engine__Ast.Make(InputLanguage).item

val item_NotImplementedYet : 
  span:Hax_engine.Ast.span ->
  ident:Hax_engine.Ast.concrete_ident ->
  attrs:Hax_engine.Ast.attrs ->
  Hax_engine__Ast.Make(InputLanguage).item

val guard_IfLet : 
  span:Hax_engine.Ast.span ->
  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

module NoSpan : sig ... end

val ty_tuple : AST.ty Hax_engine.Prelude.list -> AST.ty

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

module Explicit : sig ... end

val ty_unit : AST.ty

val expr_unit : 
  span:Hax_engine.Ast.span ->
  Hax_engine__Ast.Make(InputLanguage).expr

val expr_tuple : 
  span:Hax_engine.Ast.span ->
  AST.expr Hax_engine.Prelude.list ->
  AST.expr

val pat_PBinding : 
  typ:Hax_engine__Ast.Make(InputLanguage).ty ->
  span:Hax_engine.Ast.span ->
  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 arm : 
  span:Hax_engine.Span.t ->
  AST.pat ->
  ?guard:AST.guard Hax_engine.Prelude.option ->
  AST.expr ->
  AST.arm

val pat_Constructor_CF : 
  span:Hax_engine.Ast.span ->
  typ:AST.ty ->
  [ `Break | `Continue ] ->
  AST.pat ->
  AST.pat

val call_Constructor' : 
  Hax_engine.Ast.global_ident ->
  Hax_engine.Prelude.bool ->
  AST.expr Hax_engine.Prelude.list ->
  Hax_engine.Span.t ->
  AST.ty ->
  AST.expr

val call_Constructor : 
  Hax_engine.Concrete_ident.name ->
  Hax_engine.Prelude.bool ->
  AST.expr Hax_engine.Prelude.list ->
  Hax_engine.Span.t ->
  AST.ty ->
  AST.expr

val expr'_Constructor_CF : 
  span:Hax_engine.Ast.span ->
  break_type:AST.ty ->
  ?continue_type:AST.ty ->
  [ `Break | `Continue ] ->
  AST.expr ->
  AST.expr

val expr_Constructor_CF : 
  span:Hax_engine.Ast.span ->
  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

module Make0 (Span : sig ... end) : sig ... end

module type S = sig ... end

module Make (Span : sig ... end) : sig ... end

val make : Hax_engine.Ast.span -> (module S)