Module Fstar_backend.AST

type safety_kind =
  1. | Safe
  2. | Unsafe of InputLanguage.unsafe
val pp_safety_kind : Ppx_deriving_runtime.Format.formatter -> safety_kind -> Ppx_deriving_runtime.unit
val show_safety_kind : safety_kind -> Ppx_deriving_runtime.string
val equal_safety_kind : safety_kind -> safety_kind -> Ppx_deriving_runtime.bool
val safety_kind_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> safety_kind
val yojson_of_safety_kind : safety_kind -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_safety_kind : safety_kind -> safety_kind -> Hax_engine.Prelude.int
val safety_kind_of_sexp : Sexplib0.Sexp.t -> safety_kind
val sexp_of_safety_kind : safety_kind -> Sexplib0.Sexp.t
val hash_fold_safety_kind : Ppx_hash_lib.Std.Hash.state -> safety_kind -> Ppx_hash_lib.Std.Hash.state
val hash_safety_kind : safety_kind -> Ppx_hash_lib.Std.Hash.hash_value
type borrow_kind =
  1. | Shared
  2. | Unique
  3. | Mut of InputLanguage.mutable_reference
val pp_borrow_kind : Ppx_deriving_runtime.Format.formatter -> borrow_kind -> Ppx_deriving_runtime.unit
val show_borrow_kind : borrow_kind -> Ppx_deriving_runtime.string
val equal_borrow_kind : borrow_kind -> borrow_kind -> Ppx_deriving_runtime.bool
val borrow_kind_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> borrow_kind
val yojson_of_borrow_kind : borrow_kind -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_borrow_kind : borrow_kind -> borrow_kind -> Hax_engine.Prelude.int
val borrow_kind_of_sexp : Sexplib0.Sexp.t -> borrow_kind
val sexp_of_borrow_kind : borrow_kind -> Sexplib0.Sexp.t
val hash_fold_borrow_kind : Ppx_hash_lib.Std.Hash.state -> borrow_kind -> Ppx_hash_lib.Std.Hash.state
val hash_borrow_kind : borrow_kind -> Ppx_hash_lib.Std.Hash.hash_value
type binding_mode =
  1. | ByValue
  2. | ByRef of borrow_kind * InputLanguage.reference
val pp_binding_mode : Ppx_deriving_runtime.Format.formatter -> binding_mode -> Ppx_deriving_runtime.unit
val show_binding_mode : binding_mode -> Ppx_deriving_runtime.string
val equal_binding_mode : binding_mode -> binding_mode -> Ppx_deriving_runtime.bool
val binding_mode_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> binding_mode
val yojson_of_binding_mode : binding_mode -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_binding_mode : binding_mode -> binding_mode -> Hax_engine.Prelude.int
val binding_mode_of_sexp : Sexplib0.Sexp.t -> binding_mode
val sexp_of_binding_mode : binding_mode -> Sexplib0.Sexp.t
val hash_fold_binding_mode : Ppx_hash_lib.Std.Hash.state -> binding_mode -> Ppx_hash_lib.Std.Hash.state
val hash_binding_mode : binding_mode -> Ppx_hash_lib.Std.Hash.hash_value
type ty =
  1. | TBool
  2. | TChar
  3. | TStr
  4. | TApp of {
    1. ident : [ `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 ] ];
    2. args : generic_value Hax_engine.Prelude.list;
    }
  5. | TArray of {
    1. typ : ty;
    2. length : expr;
    }
  6. | TSlice of {
    1. witness : InputLanguage.slice;
    2. ty : ty;
    }
  7. | TRawPointer of {
    1. witness : InputLanguage.raw_pointer;
    }
  8. | TParam of Hax_engine.Local_ident.t
  9. | TArrow of ty Hax_engine.Prelude.list * ty
  10. | TAssociatedType of {
    1. impl : impl_expr;
    2. item : Hax_engine.Concrete_ident.t;
    }
  11. | TOpaque of Hax_engine.Concrete_ident.t
  12. | TDyn of {
    1. witness : InputLanguage.dyn;
    2. goals : dyn_trait_goal Hax_engine.Prelude.list;
    }
and generic_value =
  1. | GLifetime of {
    1. lt : Hax_engine.Prelude.string;
    2. witness : InputLanguage.lifetime;
    }
  2. | GType of ty
  3. | GConst of expr
and impl_expr = {
  1. kind : impl_expr_kind;
  2. goal : trait_goal;
}
and impl_expr_kind =
  1. | Self
  2. | Concrete of trait_goal
  3. | LocalBound of {
    1. id : Hax_engine.Prelude.string;
    }
  4. | Parent of {
    1. impl : impl_expr;
    2. ident : impl_ident;
    }
  5. | Projection of {
    1. impl : impl_expr;
    2. item : Hax_engine.Concrete_ident.t;
    3. ident : impl_ident;
    }
  6. | ImplApp of {
    1. impl : impl_expr;
    2. args : impl_expr Hax_engine.Prelude.list;
    }
  7. | Dyn
  8. | Builtin of trait_goal
and dyn_trait_goal = {
  1. trait : Hax_engine.Concrete_ident.t;
  2. non_self_args : generic_value Hax_engine.Prelude.list;
}
and impl_ident = {
  1. goal : trait_goal;
  2. name : Hax_engine.Prelude.string;
}
and projection_predicate = {
  1. impl : impl_expr;
  2. assoc_item : Hax_engine.Concrete_ident.t;
  3. typ : ty;
}
and pat' =
  1. | PWild
  2. | PAscription of {
    1. typ : ty;
    2. typ_span : Hax_engine.Span.t;
    3. pat : pat;
    }
  3. | PConstruct of {
    1. constructor : [ `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 ] ];
    2. is_record : Hax_engine.Prelude.bool;
    3. is_struct : Hax_engine.Prelude.bool;
    4. fields : field_pat Hax_engine.Prelude.list;
    }
  4. | POr of {
    1. subpats : pat Hax_engine.Prelude.list;
    }
  5. | PArray of {
    1. args : pat Hax_engine.Prelude.list;
    }
  6. | PDeref of {
    1. subpat : pat;
    2. witness : InputLanguage.reference;
    }
and pat = {
  1. p : pat';
  2. span : Hax_engine.Span.t;
  3. typ : ty;
}
and field_pat = {
  1. field : [ `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 ] ];
  2. pat : pat;
}
and cf_kind =
  1. | BreakOnly
  2. | BreakOrReturn
and expr' =
  1. | If of {
    1. cond : expr;
    2. then_ : expr;
    3. else_ : expr Hax_engine.Prelude.option;
    }
  2. | App of {
    1. f : expr;
    2. args : expr Hax_engine.Prelude.list;
    3. generic_args : generic_value Hax_engine.Prelude.list;
    4. bounds_impls : impl_expr Hax_engine.Prelude.list;
    5. trait : (impl_expr * generic_value Hax_engine.Prelude.list) Hax_engine.Prelude.option;
    }
  3. | Array of expr Hax_engine.Prelude.list
  4. | Construct of {
    1. constructor : [ `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 ] ];
    2. is_record : Hax_engine.Prelude.bool;
    3. is_struct : Hax_engine.Prelude.bool;
    4. fields : ([ `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 ] ] * expr) Hax_engine.Prelude.list;
    5. base : (expr * InputLanguage.construct_base) Hax_engine.Prelude.option;
    }
  5. | Match of {
    1. scrutinee : expr;
    2. arms : arm Hax_engine.Prelude.list;
    }
  6. | Let of {
    1. monadic : (supported_monads * InputLanguage.monadic_binding) Hax_engine.Prelude.option;
    2. lhs : pat;
    3. rhs : expr;
    4. body : expr;
    }
  7. | Block of {
    1. e : expr;
    2. safety_mode : safety_kind;
    3. witness : InputLanguage.block;
    }
  8. | LocalVar of Hax_engine.Local_ident.t
  9. | GlobalVar of [ `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 ] ]
  10. | Ascription of {
    1. e : expr;
    2. typ : ty;
    }
  11. | MacroInvokation of {
    1. macro : [ `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 ] ];
    2. args : Hax_engine.Prelude.string;
    3. witness : InputLanguage.macro;
    }
  12. | Assign of {
    1. lhs : lhs;
    2. e : expr;
    3. witness : InputLanguage.mutable_variable;
    }
  13. | Loop of {
    1. body : expr;
    2. kind : loop_kind;
    3. state : loop_state Hax_engine.Prelude.option;
    4. control_flow : (cf_kind * InputLanguage.fold_like_loop) Hax_engine.Prelude.option;
    5. label : Hax_engine.Prelude.string Hax_engine.Prelude.option;
    6. witness : InputLanguage.loop;
    }
  14. | Break of {
    1. e : expr;
    2. acc : (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;
    }
  15. | Return of {
    1. e : expr;
    2. witness : InputLanguage.early_exit;
    }
  16. | QuestionMark of {
    1. e : expr;
    2. return_typ : ty;
    3. witness : InputLanguage.question_mark;
    }
  17. | Continue of {
    1. acc : (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;
    }
  18. | Borrow of {
    1. kind : borrow_kind;
    2. e : expr;
    3. witness : InputLanguage.reference;
    }
  19. | Closure of {
    1. params : pat Hax_engine.Prelude.list;
    2. body : expr;
    3. captures : expr Hax_engine.Prelude.list;
    }
  20. | EffectAction of {
    1. action : InputLanguage.monadic_action;
    2. argument : expr;
    }
  21. | Quote of quote
and expr = {
  1. e : expr';
  2. span : Hax_engine.Span.t;
  3. typ : ty;
}
and quote = {
  1. contents : [ `Expr of expr | `Pat of pat | `Typ of ty | `Verbatim of Hax_engine.Prelude.string ] Hax_engine.Prelude.list;
  2. witness : InputLanguage.quote;
}
and supported_monads =
  1. | MException of ty
  2. | MResult of ty
  3. | MOption
and loop_kind =
  1. | UnconditionalLoop
  2. | WhileLoop of {
    1. condition : expr;
    2. witness : InputLanguage.while_loop;
    }
  3. | ForLoop of {
    1. pat : pat;
    2. it : expr;
    3. witness : InputLanguage.for_loop;
    }
  4. | ForIndexLoop of {
    1. start : expr;
    2. end_ : expr;
    3. var : Hax_engine.Local_ident.t;
    4. var_typ : ty;
    5. witness : InputLanguage.for_index_loop;
    }
and loop_state = {
  1. init : expr;
  2. bpat : pat;
  3. witness : InputLanguage.state_passing_loop;
}
and lhs =
  1. | LhsLocalVar of {
    1. var : Hax_engine.Local_ident.t;
    2. typ : ty;
    }
  2. | LhsArbitraryExpr of {
    1. e : expr;
    2. witness : InputLanguage.arbitrary_lhs;
    }
  3. | LhsFieldAccessor of {
    1. e : lhs;
    2. typ : ty;
    3. field : [ `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 ] ];
    4. witness : InputLanguage.nontrivial_lhs;
    }
  4. | LhsArrayAccessor of {
    1. e : lhs;
    2. typ : ty;
    3. index : expr;
    4. witness : InputLanguage.nontrivial_lhs;
    }
and guard = {
  1. guard : guard';
  2. span : Hax_engine.Span.t;
}
and guard' =
  1. | IfLet of {
    1. lhs : pat;
    2. rhs : expr;
    3. witness : InputLanguage.match_guard;
    }
and arm' = {
  1. arm_pat : pat;
  2. body : expr;
  3. guard : guard Hax_engine.Prelude.option;
}
and arm = {
  1. arm : arm';
  2. span : Hax_engine.Span.t;
}
val pp_ty : Ppx_deriving_runtime.Format.formatter -> ty -> Ppx_deriving_runtime.unit
val show_ty : ty -> Ppx_deriving_runtime.string
val pp_generic_value : Ppx_deriving_runtime.Format.formatter -> generic_value -> Ppx_deriving_runtime.unit
val show_generic_value : generic_value -> Ppx_deriving_runtime.string
val pp_impl_expr : Ppx_deriving_runtime.Format.formatter -> impl_expr -> Ppx_deriving_runtime.unit
val show_impl_expr : impl_expr -> Ppx_deriving_runtime.string
val pp_impl_expr_kind : Ppx_deriving_runtime.Format.formatter -> impl_expr_kind -> Ppx_deriving_runtime.unit
val show_impl_expr_kind : impl_expr_kind -> Ppx_deriving_runtime.string
val pp_trait_goal : Ppx_deriving_runtime.Format.formatter -> trait_goal -> Ppx_deriving_runtime.unit
val show_trait_goal : trait_goal -> Ppx_deriving_runtime.string
val pp_dyn_trait_goal : Ppx_deriving_runtime.Format.formatter -> dyn_trait_goal -> Ppx_deriving_runtime.unit
val show_dyn_trait_goal : dyn_trait_goal -> Ppx_deriving_runtime.string
val pp_impl_ident : Ppx_deriving_runtime.Format.formatter -> impl_ident -> Ppx_deriving_runtime.unit
val show_impl_ident : impl_ident -> Ppx_deriving_runtime.string
val pp_projection_predicate : Ppx_deriving_runtime.Format.formatter -> projection_predicate -> Ppx_deriving_runtime.unit
val show_projection_predicate : projection_predicate -> Ppx_deriving_runtime.string
val pp_pat' : Ppx_deriving_runtime.Format.formatter -> pat' -> Ppx_deriving_runtime.unit
val show_pat' : pat' -> Ppx_deriving_runtime.string
val pp_pat : Ppx_deriving_runtime.Format.formatter -> pat -> Ppx_deriving_runtime.unit
val show_pat : pat -> Ppx_deriving_runtime.string
val pp_field_pat : Ppx_deriving_runtime.Format.formatter -> field_pat -> Ppx_deriving_runtime.unit
val show_field_pat : field_pat -> Ppx_deriving_runtime.string
val pp_cf_kind : Ppx_deriving_runtime.Format.formatter -> cf_kind -> Ppx_deriving_runtime.unit
val show_cf_kind : cf_kind -> Ppx_deriving_runtime.string
val pp_expr' : Ppx_deriving_runtime.Format.formatter -> expr' -> Ppx_deriving_runtime.unit
val show_expr' : expr' -> Ppx_deriving_runtime.string
val pp_expr : Ppx_deriving_runtime.Format.formatter -> expr -> Ppx_deriving_runtime.unit
val show_expr : expr -> Ppx_deriving_runtime.string
val pp_quote : Ppx_deriving_runtime.Format.formatter -> quote -> Ppx_deriving_runtime.unit
val show_quote : quote -> Ppx_deriving_runtime.string
val pp_supported_monads : Ppx_deriving_runtime.Format.formatter -> supported_monads -> Ppx_deriving_runtime.unit
val show_supported_monads : supported_monads -> Ppx_deriving_runtime.string
val pp_loop_kind : Ppx_deriving_runtime.Format.formatter -> loop_kind -> Ppx_deriving_runtime.unit
val show_loop_kind : loop_kind -> Ppx_deriving_runtime.string
val pp_loop_state : Ppx_deriving_runtime.Format.formatter -> loop_state -> Ppx_deriving_runtime.unit
val show_loop_state : loop_state -> Ppx_deriving_runtime.string
val pp_lhs : Ppx_deriving_runtime.Format.formatter -> lhs -> Ppx_deriving_runtime.unit
val show_lhs : lhs -> Ppx_deriving_runtime.string
val pp_guard : Ppx_deriving_runtime.Format.formatter -> guard -> Ppx_deriving_runtime.unit
val show_guard : guard -> Ppx_deriving_runtime.string
val pp_guard' : Ppx_deriving_runtime.Format.formatter -> guard' -> Ppx_deriving_runtime.unit
val show_guard' : guard' -> Ppx_deriving_runtime.string
val pp_arm' : Ppx_deriving_runtime.Format.formatter -> arm' -> Ppx_deriving_runtime.unit
val show_arm' : arm' -> Ppx_deriving_runtime.string
val pp_arm : Ppx_deriving_runtime.Format.formatter -> arm -> Ppx_deriving_runtime.unit
val show_arm : arm -> Ppx_deriving_runtime.string
val equal_ty : ty -> ty -> Ppx_deriving_runtime.bool
val equal_generic_value : generic_value -> generic_value -> Ppx_deriving_runtime.bool
val equal_impl_expr : impl_expr -> impl_expr -> Ppx_deriving_runtime.bool
val equal_impl_expr_kind : impl_expr_kind -> impl_expr_kind -> Ppx_deriving_runtime.bool
val equal_trait_goal : trait_goal -> trait_goal -> Ppx_deriving_runtime.bool
val equal_dyn_trait_goal : dyn_trait_goal -> dyn_trait_goal -> Ppx_deriving_runtime.bool
val equal_impl_ident : impl_ident -> impl_ident -> Ppx_deriving_runtime.bool
val equal_projection_predicate : projection_predicate -> projection_predicate -> Ppx_deriving_runtime.bool
val equal_pat' : pat' -> pat' -> Ppx_deriving_runtime.bool
val equal_pat : pat -> pat -> Ppx_deriving_runtime.bool
val equal_field_pat : field_pat -> field_pat -> Ppx_deriving_runtime.bool
val equal_cf_kind : cf_kind -> cf_kind -> Ppx_deriving_runtime.bool
val equal_expr' : expr' -> expr' -> Ppx_deriving_runtime.bool
val equal_expr : expr -> expr -> Ppx_deriving_runtime.bool
val equal_quote : quote -> quote -> Ppx_deriving_runtime.bool
val equal_supported_monads : supported_monads -> supported_monads -> Ppx_deriving_runtime.bool
val equal_loop_kind : loop_kind -> loop_kind -> Ppx_deriving_runtime.bool
val equal_loop_state : loop_state -> loop_state -> Ppx_deriving_runtime.bool
val equal_lhs : lhs -> lhs -> Ppx_deriving_runtime.bool
val equal_guard : guard -> guard -> Ppx_deriving_runtime.bool
val equal_guard' : guard' -> guard' -> Ppx_deriving_runtime.bool
val equal_arm' : arm' -> arm' -> Ppx_deriving_runtime.bool
val equal_arm : arm -> arm -> Ppx_deriving_runtime.bool
val ty_of_yojson : Yojson.Safe.t -> ty
val generic_value_of_yojson : Yojson.Safe.t -> generic_value
val impl_expr_of_yojson : Yojson.Safe.t -> impl_expr
val impl_expr_kind_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> impl_expr_kind
val trait_goal_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> trait_goal
val dyn_trait_goal_of_yojson : Yojson.Safe.t -> dyn_trait_goal
val impl_ident_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> impl_ident
val projection_predicate_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> projection_predicate
val pat'_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> pat'
val pat_of_yojson : Yojson.Safe.t -> pat
val field_pat_of_yojson : Yojson.Safe.t -> field_pat
val cf_kind_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> cf_kind
val expr'_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> expr'
val expr_of_yojson : Yojson.Safe.t -> expr
val quote_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> quote
val supported_monads_of_yojson : Yojson.Safe.t -> supported_monads
val loop_kind_of_yojson : Yojson.Safe.t -> loop_kind
val loop_state_of_yojson : Yojson.Safe.t -> loop_state
val lhs_of_yojson : Yojson.Safe.t -> lhs
val guard_of_yojson : Yojson.Safe.t -> guard
val guard'_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> guard'
val arm'_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> arm'
val arm_of_yojson : Yojson.Safe.t -> arm
val yojson_of_ty : ty -> Yojson.Safe.t
val yojson_of_generic_value : generic_value -> Yojson.Safe.t
val yojson_of_impl_expr : impl_expr -> Yojson.Safe.t
val yojson_of_impl_expr_kind : impl_expr_kind -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_trait_goal : trait_goal -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_dyn_trait_goal : dyn_trait_goal -> Yojson.Safe.t
val yojson_of_impl_ident : impl_ident -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_projection_predicate : projection_predicate -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_pat' : pat' -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_pat : pat -> Yojson.Safe.t
val yojson_of_field_pat : field_pat -> Yojson.Safe.t
val yojson_of_cf_kind : cf_kind -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_expr' : expr' -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_expr : expr -> Yojson.Safe.t
val yojson_of_quote : quote -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_supported_monads : supported_monads -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_loop_kind : loop_kind -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_loop_state : loop_state -> Yojson.Safe.t
val yojson_of_lhs : lhs -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_guard : guard -> Yojson.Safe.t
val yojson_of_guard' : guard' -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_arm' : arm' -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_arm : arm -> Yojson.Safe.t
val compare_ty : ty -> ty -> Hax_engine.Prelude.int
val compare_generic_value : generic_value -> generic_value -> Hax_engine.Prelude.int
val compare_impl_expr : impl_expr -> impl_expr -> Hax_engine.Prelude.int
val compare_impl_expr_kind : impl_expr_kind -> impl_expr_kind -> Hax_engine.Prelude.int
val compare_trait_goal : trait_goal -> trait_goal -> Hax_engine.Prelude.int
val compare_dyn_trait_goal : dyn_trait_goal -> dyn_trait_goal -> Hax_engine.Prelude.int
val compare_impl_ident : impl_ident -> impl_ident -> Hax_engine.Prelude.int
val compare_projection_predicate : projection_predicate -> projection_predicate -> Hax_engine.Prelude.int
val compare_pat' : pat' -> pat' -> Hax_engine.Prelude.int
val compare_pat : pat -> pat -> Hax_engine.Prelude.int
val compare_field_pat : field_pat -> field_pat -> Hax_engine.Prelude.int
val compare_cf_kind : cf_kind -> cf_kind -> Hax_engine.Prelude.int
val compare_expr' : expr' -> expr' -> Hax_engine.Prelude.int
val compare_expr : expr -> expr -> Hax_engine.Prelude.int
val compare_quote : quote -> quote -> Hax_engine.Prelude.int
val compare_supported_monads : supported_monads -> supported_monads -> Hax_engine.Prelude.int
val compare_loop_kind : loop_kind -> loop_kind -> Hax_engine.Prelude.int
val compare_loop_state : loop_state -> loop_state -> Hax_engine.Prelude.int
val compare_lhs : lhs -> lhs -> Hax_engine.Prelude.int
val compare_guard : guard -> guard -> Hax_engine.Prelude.int
val compare_guard' : guard' -> guard' -> Hax_engine.Prelude.int
val compare_arm' : arm' -> arm' -> Hax_engine.Prelude.int
val compare_arm : arm -> arm -> Hax_engine.Prelude.int
val ty_of_sexp : Sexplib0__.Sexp.t -> ty
val generic_value_of_sexp : Sexplib0.Sexp.t -> generic_value
val impl_expr_of_sexp : Sexplib0.Sexp.t -> impl_expr
val impl_expr_kind_of_sexp : Sexplib0__.Sexp.t -> impl_expr_kind
val trait_goal_of_sexp : Sexplib0__.Sexp.t -> trait_goal
val dyn_trait_goal_of_sexp : Sexplib0.Sexp.t -> dyn_trait_goal
val impl_ident_of_sexp : Sexplib0__.Sexp.t -> impl_ident
val projection_predicate_of_sexp : Sexplib0.Sexp.t -> projection_predicate
val pat'_of_sexp : Sexplib0__.Sexp.t -> pat'
val pat_of_sexp : Sexplib0__.Sexp.t -> pat
val field_pat_of_sexp : Sexplib0.Sexp.t -> field_pat
val cf_kind_of_sexp : Sexplib0.Sexp.t -> cf_kind
val expr'_of_sexp : Sexplib0__.Sexp.t -> expr'
val expr_of_sexp : Sexplib0__.Sexp.t -> expr
val quote_of_sexp : Sexplib0.Sexp.t -> quote
val supported_monads_of_sexp : Sexplib0.Sexp.t -> supported_monads
val loop_kind_of_sexp : Sexplib0__.Sexp.t -> loop_kind
val loop_state_of_sexp : Sexplib0.Sexp.t -> loop_state
val lhs_of_sexp : Sexplib0__.Sexp.t -> lhs
val guard_of_sexp : Sexplib0.Sexp.t -> guard
val guard'_of_sexp : Sexplib0__.Sexp.t -> guard'
val arm'_of_sexp : Sexplib0__.Sexp.t -> arm'
val arm_of_sexp : Sexplib0.Sexp.t -> arm
val sexp_of_ty : ty -> Sexplib0.Sexp.t
val sexp_of_generic_value : generic_value -> Sexplib0.Sexp.t
val sexp_of_impl_expr : impl_expr -> Sexplib0.Sexp.t
val sexp_of_impl_expr_kind : impl_expr_kind -> Sexplib0.Sexp.t
val sexp_of_trait_goal : trait_goal -> Sexplib0.Sexp.t
val sexp_of_dyn_trait_goal : dyn_trait_goal -> Sexplib0.Sexp.t
val sexp_of_impl_ident : impl_ident -> Sexplib0.Sexp.t
val sexp_of_projection_predicate : projection_predicate -> Sexplib0.Sexp.t
val sexp_of_pat' : pat' -> Sexplib0.Sexp.t
val sexp_of_pat : pat -> Sexplib0.Sexp.t
val sexp_of_field_pat : field_pat -> Sexplib0.Sexp.t
val sexp_of_cf_kind : cf_kind -> Sexplib0.Sexp.t
val sexp_of_expr' : expr' -> Sexplib0.Sexp.t
val sexp_of_expr : expr -> Sexplib0.Sexp.t
val sexp_of_quote : quote -> Sexplib0.Sexp.t
val sexp_of_supported_monads : supported_monads -> Sexplib0.Sexp.t
val sexp_of_loop_kind : loop_kind -> Sexplib0.Sexp.t
val sexp_of_loop_state : loop_state -> Sexplib0.Sexp.t
val sexp_of_lhs : lhs -> Sexplib0.Sexp.t
val sexp_of_guard : guard -> Sexplib0.Sexp.t
val sexp_of_guard' : guard' -> Sexplib0.Sexp.t
val sexp_of_arm' : arm' -> Sexplib0.Sexp.t
val sexp_of_arm : arm -> Sexplib0.Sexp.t
val hash_fold_ty : Base__.Ppx_hash_lib.Std.Hash.state -> ty -> Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_generic_value : Base__.Ppx_hash_lib.Std.Hash.state -> generic_value -> Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_impl_expr : Base__.Ppx_hash_lib.Std.Hash.state -> impl_expr -> Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_impl_expr_kind : Ppx_hash_lib.Std.Hash.state -> impl_expr_kind -> Ppx_hash_lib.Std.Hash.state
val hash_fold_trait_goal : Ppx_hash_lib.Std.Hash.state -> trait_goal -> Ppx_hash_lib.Std.Hash.state
val hash_fold_dyn_trait_goal : Base__.Ppx_hash_lib.Std.Hash.state -> dyn_trait_goal -> Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_impl_ident : Ppx_hash_lib.Std.Hash.state -> impl_ident -> Ppx_hash_lib.Std.Hash.state
val hash_fold_projection_predicate : Ppx_hash_lib.Std.Hash.state -> projection_predicate -> Ppx_hash_lib.Std.Hash.state
val hash_fold_pat' : Ppx_hash_lib.Std.Hash.state -> pat' -> Ppx_hash_lib.Std.Hash.state
val hash_fold_pat : Base__.Ppx_hash_lib.Std.Hash.state -> pat -> Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_field_pat : Base__.Ppx_hash_lib.Std.Hash.state -> field_pat -> Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_cf_kind : Ppx_hash_lib.Std.Hash.state -> cf_kind -> Ppx_hash_lib.Std.Hash.state
val hash_fold_expr' : Ppx_hash_lib.Std.Hash.state -> expr' -> Ppx_hash_lib.Std.Hash.state
val hash_fold_expr : Base__.Ppx_hash_lib.Std.Hash.state -> expr -> Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_quote : Ppx_hash_lib.Std.Hash.state -> quote -> Ppx_hash_lib.Std.Hash.state
val hash_fold_supported_monads : Ppx_hash_lib.Std.Hash.state -> supported_monads -> Ppx_hash_lib.Std.Hash.state
val hash_fold_loop_kind : Ppx_hash_lib.Std.Hash.state -> loop_kind -> Ppx_hash_lib.Std.Hash.state
val hash_fold_loop_state : Base__.Ppx_hash_lib.Std.Hash.state -> loop_state -> Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_lhs : Ppx_hash_lib.Std.Hash.state -> lhs -> Ppx_hash_lib.Std.Hash.state
val hash_fold_guard : Base__.Ppx_hash_lib.Std.Hash.state -> guard -> Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_guard' : Ppx_hash_lib.Std.Hash.state -> guard' -> Ppx_hash_lib.Std.Hash.state
val hash_fold_arm' : Ppx_hash_lib.Std.Hash.state -> arm' -> Ppx_hash_lib.Std.Hash.state
val hash_fold_arm : Base__.Ppx_hash_lib.Std.Hash.state -> arm -> Base__.Ppx_hash_lib.Std.Hash.state
val hash_ty : ty -> Ppx_hash_lib.Std.Hash.hash_value
val hash_generic_value : generic_value -> Ppx_hash_lib.Std.Hash.hash_value
val hash_impl_expr : impl_expr -> Ppx_hash_lib.Std.Hash.hash_value
val hash_impl_expr_kind : impl_expr_kind -> Ppx_hash_lib.Std.Hash.hash_value
val hash_trait_goal : trait_goal -> Ppx_hash_lib.Std.Hash.hash_value
val hash_dyn_trait_goal : dyn_trait_goal -> Ppx_hash_lib.Std.Hash.hash_value
val hash_impl_ident : impl_ident -> Ppx_hash_lib.Std.Hash.hash_value
val hash_projection_predicate : projection_predicate -> Ppx_hash_lib.Std.Hash.hash_value
val hash_pat' : pat' -> Ppx_hash_lib.Std.Hash.hash_value
val hash_pat : pat -> Ppx_hash_lib.Std.Hash.hash_value
val hash_field_pat : field_pat -> Ppx_hash_lib.Std.Hash.hash_value
val hash_cf_kind : cf_kind -> Ppx_hash_lib.Std.Hash.hash_value
val hash_expr' : expr' -> Ppx_hash_lib.Std.Hash.hash_value
val hash_expr : expr -> Ppx_hash_lib.Std.Hash.hash_value
val hash_quote : quote -> Ppx_hash_lib.Std.Hash.hash_value
val hash_supported_monads : supported_monads -> Ppx_hash_lib.Std.Hash.hash_value
val hash_loop_kind : loop_kind -> Ppx_hash_lib.Std.Hash.hash_value
val hash_loop_state : loop_state -> Ppx_hash_lib.Std.Hash.hash_value
val hash_lhs : lhs -> Ppx_hash_lib.Std.Hash.hash_value
val hash_guard : guard -> Ppx_hash_lib.Std.Hash.hash_value
val hash_guard' : guard' -> Ppx_hash_lib.Std.Hash.hash_value
val hash_arm' : arm' -> Ppx_hash_lib.Std.Hash.hash_value
val hash_arm : arm -> Ppx_hash_lib.Std.Hash.hash_value
type generic_param = {
  1. ident : Hax_engine.Local_ident.t;
  2. span : Hax_engine.Span.t;
  3. attrs : Hax_engine__Ast.attr Hax_engine.Prelude.list;
  4. kind : generic_param_kind;
}
and generic_param_kind =
  1. | GPLifetime of {
    1. witness : InputLanguage.lifetime;
    }
  2. | GPType
  3. | GPConst of {
    1. typ : ty;
    }
and generic_constraint =
  1. | GCLifetime of Hax_engine.Prelude.string * InputLanguage.lifetime
  2. | GCType of impl_ident
  3. | GCProjection of projection_predicate
val pp_generic_param : Ppx_deriving_runtime.Format.formatter -> generic_param -> Ppx_deriving_runtime.unit
val show_generic_param : generic_param -> Ppx_deriving_runtime.string
val pp_generic_param_kind : Ppx_deriving_runtime.Format.formatter -> generic_param_kind -> Ppx_deriving_runtime.unit
val show_generic_param_kind : generic_param_kind -> Ppx_deriving_runtime.string
val pp_generic_constraint : Ppx_deriving_runtime.Format.formatter -> generic_constraint -> Ppx_deriving_runtime.unit
val show_generic_constraint : generic_constraint -> Ppx_deriving_runtime.string
val equal_generic_param : generic_param -> generic_param -> Ppx_deriving_runtime.bool
val equal_generic_param_kind : generic_param_kind -> generic_param_kind -> Ppx_deriving_runtime.bool
val equal_generic_constraint : generic_constraint -> generic_constraint -> Ppx_deriving_runtime.bool
val generic_param_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> generic_param
val generic_param_kind_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> generic_param_kind
val generic_constraint_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> generic_constraint
val yojson_of_generic_param : generic_param -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_generic_param_kind : generic_param_kind -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_generic_constraint : generic_constraint -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_generic_param : generic_param -> generic_param -> Hax_engine.Prelude.int
val compare_generic_param_kind : generic_param_kind -> generic_param_kind -> Hax_engine.Prelude.int
val compare_generic_constraint : generic_constraint -> generic_constraint -> Hax_engine.Prelude.int
val generic_param_of_sexp : Sexplib0.Sexp.t -> generic_param
val generic_param_kind_of_sexp : Sexplib0__.Sexp.t -> generic_param_kind
val generic_constraint_of_sexp : Sexplib0.Sexp.t -> generic_constraint
val sexp_of_generic_param : generic_param -> Sexplib0.Sexp.t
val sexp_of_generic_param_kind : generic_param_kind -> Sexplib0.Sexp.t
val sexp_of_generic_constraint : generic_constraint -> Sexplib0.Sexp.t
val hash_fold_generic_param : Ppx_hash_lib.Std.Hash.state -> generic_param -> Ppx_hash_lib.Std.Hash.state
val hash_fold_generic_param_kind : Ppx_hash_lib.Std.Hash.state -> generic_param_kind -> Ppx_hash_lib.Std.Hash.state
val hash_fold_generic_constraint : Ppx_hash_lib.Std.Hash.state -> generic_constraint -> Ppx_hash_lib.Std.Hash.state
val hash_generic_param : generic_param -> Ppx_hash_lib.Std.Hash.hash_value
val hash_generic_param_kind : generic_param_kind -> Ppx_hash_lib.Std.Hash.hash_value
val hash_generic_constraint : generic_constraint -> Ppx_hash_lib.Std.Hash.hash_value
type param = {
  1. pat : pat;
  2. typ : ty;
  3. typ_span : Hax_engine.Span.t Hax_engine.Prelude.option;
  4. attrs : Hax_engine__Ast.attr Hax_engine.Prelude.list;
}
and variant = {
  1. name : Hax_engine.Concrete_ident.t;
  2. arguments : (Hax_engine.Concrete_ident.t * ty * Hax_engine__Ast.attr Hax_engine.Prelude.list) Hax_engine.Prelude.list;
  3. is_record : Hax_engine.Prelude.bool;
  4. attrs : Hax_engine__Ast.attr Hax_engine.Prelude.list;
}
and item' =
  1. | Fn of {
    1. name : Hax_engine.Concrete_ident.t;
    2. generics : generics;
    3. body : expr;
    4. params : param Hax_engine.Prelude.list;
    5. safety : safety_kind;
    }
  2. | TyAlias of {
    1. name : Hax_engine.Concrete_ident.t;
    2. generics : generics;
    3. ty : ty;
    }
  3. | Type of {
    1. name : Hax_engine.Concrete_ident.t;
    2. generics : generics;
    3. variants : variant Hax_engine.Prelude.list;
    4. is_struct : Hax_engine.Prelude.bool;
    }
  4. | IMacroInvokation of {
    1. macro : Hax_engine.Concrete_ident.t;
    2. argument : Hax_engine.Prelude.string;
    3. span : Hax_engine.Span.t;
    4. witness : InputLanguage.macro;
    }
  5. | Trait of {
    1. name : Hax_engine.Concrete_ident.t;
    2. generics : generics;
    3. items : trait_item Hax_engine.Prelude.list;
    4. safety : safety_kind;
    }
  6. | Impl of {
    1. generics : generics;
    2. self_ty : ty;
    3. of_trait : Hax_engine.Concrete_ident.t * generic_value Hax_engine.Prelude.list;
    4. items : impl_item Hax_engine.Prelude.list;
    5. parent_bounds : (impl_expr * impl_ident) Hax_engine.Prelude.list;
    6. safety : safety_kind;
    }
  7. | Alias of {
    1. name : Hax_engine.Concrete_ident.t;
    2. item : Hax_engine.Concrete_ident.t;
    }
  8. | Use of {
    1. path : Hax_engine.Prelude.string Hax_engine.Prelude.list;
    2. is_external : Hax_engine.Prelude.bool;
    3. rename : Hax_engine.Prelude.string Hax_engine.Prelude.option;
    }
  9. | HaxError of Hax_engine.Prelude.string
  10. | NotImplementedYet
and item = {
  1. v : item';
  2. span : Hax_engine.Span.t;
  3. ident : Hax_engine.Concrete_ident.t;
  4. attrs : Hax_engine__Ast.attr Hax_engine.Prelude.list;
}
and impl_item' =
  1. | IIType of {
    1. typ : ty;
    2. parent_bounds : (impl_expr * impl_ident) Hax_engine.Prelude.list;
    }
  2. | IIFn of {
    1. body : expr;
    2. params : param Hax_engine.Prelude.list;
    }
and impl_item = {
  1. ii_span : Hax_engine.Span.t;
  2. ii_generics : generics;
  3. ii_v : impl_item';
  4. ii_ident : Hax_engine.Concrete_ident.t;
  5. ii_attrs : Hax_engine__Ast.attr Hax_engine.Prelude.list;
}
and trait_item' =
  1. | TIType of impl_ident Hax_engine.Prelude.list
  2. | TIFn of ty
  3. | TIDefault of {
    1. params : param Hax_engine.Prelude.list;
    2. body : expr;
    3. witness : InputLanguage.trait_item_default;
    }
and trait_item = {
  1. ti_span : Hax_engine.Span.t;
  2. ti_generics : generics;
  3. ti_v : trait_item';
  4. ti_ident : Hax_engine.Concrete_ident.t;
  5. ti_attrs : Hax_engine__Ast.attr Hax_engine.Prelude.list;
}
val pp_param : Ppx_deriving_runtime.Format.formatter -> param -> Ppx_deriving_runtime.unit
val show_param : param -> Ppx_deriving_runtime.string
val pp_generics : Ppx_deriving_runtime.Format.formatter -> generics -> Ppx_deriving_runtime.unit
val show_generics : generics -> Ppx_deriving_runtime.string
val pp_variant : Ppx_deriving_runtime.Format.formatter -> variant -> Ppx_deriving_runtime.unit
val show_variant : variant -> Ppx_deriving_runtime.string
val pp_item' : Ppx_deriving_runtime.Format.formatter -> item' -> Ppx_deriving_runtime.unit
val show_item' : item' -> Ppx_deriving_runtime.string
val pp_item : Ppx_deriving_runtime.Format.formatter -> item -> Ppx_deriving_runtime.unit
val show_item : item -> Ppx_deriving_runtime.string
val pp_impl_item' : Ppx_deriving_runtime.Format.formatter -> impl_item' -> Ppx_deriving_runtime.unit
val show_impl_item' : impl_item' -> Ppx_deriving_runtime.string
val pp_impl_item : Ppx_deriving_runtime.Format.formatter -> impl_item -> Ppx_deriving_runtime.unit
val show_impl_item : impl_item -> Ppx_deriving_runtime.string
val pp_trait_item' : Ppx_deriving_runtime.Format.formatter -> trait_item' -> Ppx_deriving_runtime.unit
val show_trait_item' : trait_item' -> Ppx_deriving_runtime.string
val pp_trait_item : Ppx_deriving_runtime.Format.formatter -> trait_item -> Ppx_deriving_runtime.unit
val show_trait_item : trait_item -> Ppx_deriving_runtime.string
val equal_param : param -> param -> Ppx_deriving_runtime.bool
val equal_generics : generics -> generics -> Ppx_deriving_runtime.bool
val equal_variant : variant -> variant -> Ppx_deriving_runtime.bool
val equal_item' : item' -> item' -> Ppx_deriving_runtime.bool
val equal_item : item -> item -> Ppx_deriving_runtime.bool
val equal_impl_item' : impl_item' -> impl_item' -> Ppx_deriving_runtime.bool
val equal_impl_item : impl_item -> impl_item -> Ppx_deriving_runtime.bool
val equal_trait_item' : trait_item' -> trait_item' -> Ppx_deriving_runtime.bool
val equal_trait_item : trait_item -> trait_item -> Ppx_deriving_runtime.bool
val param_of_yojson : Yojson.Safe.t -> param
val generics_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> generics
val variant_of_yojson : Yojson.Safe.t -> variant
val item'_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> item'
val item_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> item
val impl_item'_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> impl_item'
val impl_item_of_yojson : Yojson.Safe.t -> impl_item
val trait_item'_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> trait_item'
val trait_item_of_yojson : Yojson.Safe.t -> trait_item
val yojson_of_param : param -> Yojson.Safe.t
val yojson_of_generics : generics -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_variant : variant -> Yojson.Safe.t
val yojson_of_item' : item' -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_item : item -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_impl_item' : impl_item' -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_impl_item : impl_item -> Yojson.Safe.t
val yojson_of_trait_item' : trait_item' -> Ppx_yojson_conv_lib.Yojson.Safe.t
val yojson_of_trait_item : trait_item -> Yojson.Safe.t
val compare_param : param -> param -> Hax_engine.Prelude.int
val compare_generics : generics -> generics -> Hax_engine.Prelude.int
val compare_variant : variant -> variant -> Hax_engine.Prelude.int
val compare_item' : item' -> item' -> Hax_engine.Prelude.int
val compare_item : item -> item -> Hax_engine.Prelude.int
val compare_impl_item' : impl_item' -> impl_item' -> Hax_engine.Prelude.int
val compare_impl_item : impl_item -> impl_item -> Hax_engine.Prelude.int
val compare_trait_item' : trait_item' -> trait_item' -> Hax_engine.Prelude.int
val compare_trait_item : trait_item -> trait_item -> Hax_engine.Prelude.int
val param_of_sexp : Sexplib0.Sexp.t -> param
val generics_of_sexp : Sexplib0__.Sexp.t -> generics
val variant_of_sexp : Sexplib0.Sexp.t -> variant
val item'_of_sexp : Sexplib0__.Sexp.t -> item'
val item_of_sexp : Sexplib0.Sexp.t -> item
val impl_item'_of_sexp : Sexplib0__.Sexp.t -> impl_item'
val impl_item_of_sexp : Sexplib0.Sexp.t -> impl_item
val trait_item'_of_sexp : Sexplib0__.Sexp.t -> trait_item'
val trait_item_of_sexp : Sexplib0.Sexp.t -> trait_item
val sexp_of_param : param -> Sexplib0.Sexp.t
val sexp_of_generics : generics -> Sexplib0.Sexp.t
val sexp_of_variant : variant -> Sexplib0.Sexp.t
val sexp_of_item' : item' -> Sexplib0.Sexp.t
val sexp_of_item : item -> Sexplib0.Sexp.t
val sexp_of_impl_item' : impl_item' -> Sexplib0.Sexp.t
val sexp_of_impl_item : impl_item -> Sexplib0.Sexp.t
val sexp_of_trait_item' : trait_item' -> Sexplib0.Sexp.t
val sexp_of_trait_item : trait_item -> Sexplib0.Sexp.t
val hash_fold_param : Base__.Ppx_hash_lib.Std.Hash.state -> param -> Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_generics : Ppx_hash_lib.Std.Hash.state -> generics -> Ppx_hash_lib.Std.Hash.state
val hash_fold_variant : Base__.Ppx_hash_lib.Std.Hash.state -> variant -> Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_item' : Ppx_hash_lib.Std.Hash.state -> item' -> Ppx_hash_lib.Std.Hash.state
val hash_fold_item : Ppx_hash_lib.Std.Hash.state -> item -> Ppx_hash_lib.Std.Hash.state
val hash_fold_impl_item' : Ppx_hash_lib.Std.Hash.state -> impl_item' -> Ppx_hash_lib.Std.Hash.state
val hash_fold_impl_item : Base__.Ppx_hash_lib.Std.Hash.state -> impl_item -> Base__.Ppx_hash_lib.Std.Hash.state
val hash_fold_trait_item' : Ppx_hash_lib.Std.Hash.state -> trait_item' -> Ppx_hash_lib.Std.Hash.state
val hash_fold_trait_item : Base__.Ppx_hash_lib.Std.Hash.state -> trait_item -> Base__.Ppx_hash_lib.Std.Hash.state
val hash_param : param -> Ppx_hash_lib.Std.Hash.hash_value
val hash_generics : generics -> Ppx_hash_lib.Std.Hash.hash_value
val hash_variant : variant -> Ppx_hash_lib.Std.Hash.hash_value
val hash_item' : item' -> Ppx_hash_lib.Std.Hash.hash_value
val hash_item : item -> Ppx_hash_lib.Std.Hash.hash_value
val hash_impl_item' : impl_item' -> Ppx_hash_lib.Std.Hash.hash_value
val hash_impl_item : impl_item -> Ppx_hash_lib.Std.Hash.hash_value
val hash_trait_item' : trait_item' -> Ppx_hash_lib.Std.Hash.hash_value
val hash_trait_item : trait_item -> Ppx_hash_lib.Std.Hash.hash_value