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 ->
(Ast.concrete_ident * AST.expr) Prelude.list
module Mappers : sig ... end
module Reducers : sig ... end
val fresh_local_ident_in :
Ast.local_ident Prelude.list ->
Prelude.string ->
Local_ident.t
val fresh_local_ident_in_expr :
AST.expr Prelude.list ->
Prelude.string ->
Local_ident.t
val never_typ : AST.ty
val is_never_typ : AST.ty -> Prelude.bool
val unit_typ : AST.ty
val beta_reduce_closure_opt : AST.expr -> AST.expr Prelude.option
val is_unit_typ : AST.ty -> Prelude.bool
val make_lets : (AST.pat * AST.expr) Prelude.list -> AST.expr -> AST.expr
val make_var_pat : Ast.local_ident -> AST.ty -> Ast.span -> AST.pat
val ty_equality : AST.ty -> AST.ty -> Prelude.bool
val let_of_binding : (Ast.local_ident * AST.expr) -> AST.expr -> AST.expr
val lets_of_bindings :
(Ast.local_ident * AST.expr) Prelude.list ->
AST.expr ->
AST.expr
val make_tuple_typ' : AST.ty Prelude.list -> AST.ty
val make_tuple_typ : AST.ty Prelude.list -> AST.ty
val make_tuple_field_pat :
Prelude.int ->
Prelude.int ->
AST.pat ->
AST.field_pat
val make_tuple_pat'' : Span.t -> AST.field_pat Prelude.list -> AST.pat
val make_tuple_pat' : AST.pat Prelude.list -> AST.pat
val make_tuple_pat : AST.pat Prelude.list -> AST.pat
val make_tuple_expr' : span:Ast.span -> AST.expr Prelude.list -> AST.expr
val make_tuple_expr : span:Ast.span -> AST.expr Prelude.list -> AST.expr
val call_Constructor' :
Ast.global_ident ->
Prelude.bool ->
AST.expr Prelude.list ->
Span.t ->
AST.ty ->
AST.expr
val call_Constructor :
Concrete_ident.name ->
Prelude.bool ->
AST.expr Prelude.list ->
Span.t ->
AST.ty ->
AST.expr
val call' :
?impl:AST.impl_expr ->
[ `Concrete of Concrete_ident.t
| `Primitive of Hax_engine__Ast.primitive_ident
| `TupleType of Prelude.int
| `TupleCons of Prelude.int
| `TupleField of Prelude.int * Prelude.int
| `Projector of
[ `Concrete of Concrete_ident.t
| `TupleField of Prelude.int * Prelude.int ] ] ->
?generic_args:AST.generic_value Prelude.list ->
?impl_generic_args:AST.generic_value Prelude.list ->
AST.expr Prelude.list ->
Span.t ->
AST.ty ->
AST.expr
val call :
?kind:Concrete_ident.Kind.t ->
?generic_args:AST.generic_value Prelude.list ->
?impl_generic_args:AST.generic_value Prelude.list ->
?impl:AST.impl_expr ->
Concrete_ident.name ->
AST.expr Prelude.list ->
Span.t ->
AST.ty ->
AST.expr
val make_closure : AST.pat Prelude.list -> AST.expr -> Ast.span -> AST.expr
val string_lit : Span.t -> Prelude.string -> AST.expr
val hax_failure_expr' :
Span.t ->
AST.ty ->
(Diagnostics.Context.t * Diagnostics.kind) ->
Prelude.string ->
AST.expr
val hax_failure_expr :
Span.t ->
AST.ty ->
(Diagnostics.Context.t * Diagnostics.kind) ->
Ast.Full.expr ->
AST.expr
val hax_failure_typ : AST.ty
module LiftToFullAst : sig ... end
module Debug : sig ... end
val param_of_generic_const_param :
AST.generic_param ->
AST.param Prelude.option
val kind_of_item : AST.item -> Ast.item_kind
val collect_let_bindings :
AST.expr ->
(AST.pat * AST.expr) Prelude.list * AST.expr
val tuple_projector :
Span.t ->
AST.ty ->
Prelude.int ->
Prelude.int ->
AST.ty ->
AST.expr
val project_tuple :
AST.expr ->
Prelude.int ->
Prelude.int ->
AST.ty ->
AST.expr
val concat_generics : AST.generics -> AST.generics -> AST.generics
module Place : sig ... end
module StringList : sig ... end