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

module AST : sig ... end

module TypedLocalIdent : sig ... end

module Visitors : sig ... end

module M : sig ... end

module D : sig ... end

module Expect : sig ... end

module Sets : sig ... end

val functions_of_item : 
  AST.item ->
  (Hax_engine.Ast.concrete_ident * AST.expr) Hax_engine.Prelude.list

module Mappers : sig ... end

module Reducers : sig ... end

val fresh_local_ident_in : 
  Hax_engine.Ast.local_ident Hax_engine.Prelude.list ->
  Hax_engine.Prelude.string ->
  Hax_engine.Local_ident.t

val fresh_local_ident_in_expr : 
  AST.expr Hax_engine.Prelude.list ->
  Hax_engine.Prelude.string ->
  Hax_engine.Local_ident.t

val never_typ : AST.ty

val is_never_typ : AST.ty -> Hax_engine.Prelude.bool

val unit_typ : AST.ty

val unit_expr : Hax_engine.Span.t -> AST.expr

val remove_tuple1_pat : AST.pat -> AST.pat

val remove_tuple1 : AST.ty -> AST.ty

val remove_unsize : AST.expr -> AST.expr

val beta_reduce_closure_opt : AST.expr -> AST.expr Hax_engine.Prelude.option

val beta_reduce_closure : AST.expr -> AST.expr

val is_unit_typ : AST.ty -> Hax_engine.Prelude.bool

val pat_is_expr : AST.pat -> AST.expr -> Ppx_deriving_runtime.bool

val make_let : AST.pat -> AST.expr -> AST.expr -> AST.expr

val make_lets : 
  (AST.pat * AST.expr) Hax_engine.Prelude.list ->
  AST.expr ->
  AST.expr

val make_var_pat : 
  Hax_engine.Ast.local_ident ->
  AST.ty ->
  Hax_engine.Ast.span ->
  AST.pat

val ty_equality : AST.ty -> AST.ty -> Hax_engine.Prelude.bool

val let_of_binding : 
  (Hax_engine.Ast.local_ident * AST.expr) ->
  AST.expr ->
  AST.expr

val lets_of_bindings : 
  (Hax_engine.Ast.local_ident * AST.expr) Hax_engine.Prelude.list ->
  AST.expr ->
  AST.expr

val make_tuple_typ' : AST.ty Hax_engine.Prelude.list -> AST.ty

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

val make_unit_param : Hax_engine.Ast.span -> AST.param

val make_seq : AST.expr -> AST.expr -> AST.expr

val make_tuple_field_pat : 
  Hax_engine.Prelude.int ->
  Hax_engine.Prelude.int ->
  AST.pat ->
  AST.field_pat

val make_tuple_pat'' : 
  Hax_engine.Span.t ->
  AST.field_pat Hax_engine.Prelude.list ->
  AST.pat

val make_tuple_pat' : AST.pat Hax_engine.Prelude.list -> AST.pat

val make_tuple_pat : AST.pat Hax_engine.Prelude.list -> AST.pat

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

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

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 call' : 
  ?impl:AST.impl_expr ->
  [ `Concrete of Hax_engine.Concrete_ident.t
  | `Primitive of Hax_engine__Ast.primitive_ident
  | `TupleType of Hax_engine.Prelude.int
  | `TupleCons of Hax_engine.Prelude.int
  | `TupleField of Hax_engine.Prelude.int * Hax_engine.Prelude.int
  | `Projector of
    [ `Concrete of Hax_engine.Concrete_ident.t
    | `TupleField of Hax_engine.Prelude.int * Hax_engine.Prelude.int ] ] ->
  ?generic_args:AST.generic_value Hax_engine.Prelude.list ->
  ?impl_generic_args:AST.generic_value Hax_engine.Prelude.list ->
  AST.expr Hax_engine.Prelude.list ->
  Hax_engine.Span.t ->
  AST.ty ->
  AST.expr

val call : 
  ?kind:Hax_engine.Concrete_ident.Kind.t ->
  ?generic_args:AST.generic_value Hax_engine.Prelude.list ->
  ?impl_generic_args:AST.generic_value Hax_engine.Prelude.list ->
  ?impl:AST.impl_expr ->
  Hax_engine.Concrete_ident.name ->
  AST.expr Hax_engine.Prelude.list ->
  Hax_engine.Span.t ->
  AST.ty ->
  AST.expr

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

val string_lit : Hax_engine.Span.t -> Hax_engine.Prelude.string -> AST.expr

val hax_failure_expr' : 
  Hax_engine.Span.t ->
  AST.ty ->
  (Hax_engine.Diagnostics.Context.t * Hax_engine.Diagnostics.kind) ->
  Hax_engine.Prelude.string ->
  AST.expr

val hax_failure_expr : 
  Hax_engine.Span.t ->
  AST.ty ->
  (Hax_engine.Diagnostics.Context.t * Hax_engine.Diagnostics.kind) ->
  Hax_engine.Ast.Full.expr ->
  AST.expr

val hax_failure_typ : AST.ty

module LiftToFullAst : sig ... end

module Debug : sig ... end

val unbox_expr' : (AST.expr -> AST.expr) -> AST.expr -> AST.expr

val underef_expr' : (AST.expr -> AST.expr) -> AST.expr -> AST.expr

val unbox_expr : AST.expr -> AST.expr

val underef_expr : AST.expr -> AST.expr

val unbox_underef_expr : AST.expr -> AST.expr

val param_of_generic_const_param : 
  AST.generic_param ->
  AST.param Hax_engine.Prelude.option

val kind_of_item : AST.item -> Hax_engine.Ast.item_kind

val expr_of_lhs : Hax_engine.Ast.span -> AST.lhs -> AST.expr

val collect_let_bindings' : 
  AST.expr ->
  (AST.pat * AST.expr * AST.ty) Hax_engine.Prelude.list * AST.expr

val collect_let_bindings : 
  AST.expr ->
  (AST.pat * AST.expr) Hax_engine.Prelude.list * AST.expr

val map_body_of_nested_lets : (AST.expr -> AST.expr) -> AST.expr -> AST.expr

val tuple_projector : 
  Hax_engine.Span.t ->
  AST.ty ->
  Hax_engine.Prelude.int ->
  Hax_engine.Prelude.int ->
  AST.ty ->
  AST.expr

val project_tuple : 
  AST.expr ->
  Hax_engine.Prelude.int ->
  Hax_engine.Prelude.int ->
  AST.ty ->
  AST.expr

val concat_generics : AST.generics -> AST.generics -> AST.generics

module Place : sig ... end

module StringList : sig ... end