Attrs.WithItems
module I : sig ... end
val item_uid_map :
(Hax_engine__Attr_payloads.UId.T.t,
AST.item,
Base__Comparator.Make(Hax_engine__Attr_payloads.UId.T).comparator_witness)
Base__Map.t
val try_item_of_uid :
Hax_engine__Attr_payloads.UId.T.t ->
AST.item Prelude.option
val item_of_uid : Hax_engine__Attr_payloads.UId.T.t -> AST.item
val associated_items_per_roles :
Ast.attrs ->
(Hax_engine__Attr_payloads.AssocRole.T.t,
AST.item Prelude.list,
Base__Comparator.Make(Hax_engine__Attr_payloads.AssocRole.T).comparator_witness)
Base__Map.t
val associated_item :
Hax_engine__Attr_payloads.AssocRole.T.t ->
Ast.attrs ->
AST.item Prelude.option
val associated_fn :
Hax_engine__Attr_payloads.AssocRole.T.t ->
Ast.attrs ->
(AST.generics * AST.param Prelude.list * AST.expr) Prelude.option
val associated_expr :
?keep_last_args:Prelude.int ->
Hax_engine__Attr_payloads.AssocRole.T.t ->
Ast.attrs ->
AST.expr Prelude.option
val associated_items :
Hax_engine__Attr_payloads.AssocRole.T.t ->
Ast.attrs ->
AST.item Prelude.list
val associated_fns :
Hax_engine__Attr_payloads.AssocRole.T.t ->
Ast.attrs ->
(AST.generics * AST.param Prelude.list * AST.expr) Prelude.list
val associated_exprs :
?keep_last_args:Prelude.int ->
Hax_engine__Attr_payloads.AssocRole.T.t ->
Ast.attrs ->
AST.expr Prelude.list
val expect_fn : AST.item -> AST.generics * AST.param Prelude.list * AST.expr
val expect_expr :
?keep_last_args:Prelude.int ->
(AST.generics * AST.param Prelude.list * AST.expr) ->
AST.expr
val associated_refinement_in_type :
Ast.span ->
Prelude.string Prelude.list ->
Ast.attrs ->
AST.expr Prelude.option
val find_unique_attr :
Ast.attrs ->
f:(Types.ha_payload -> 'a Prelude.option) ->
'a Prelude.option
val status : Ast.attrs -> Types.ha_item_status
val late_skip : Ast.attrs -> Prelude.bool
val is_erased : Ast.attrs -> Prelude.bool
val uid : Ast.attrs -> Hax_engine__Attr_payloads.UId.T.t Prelude.option
val lemma : Ast.attrs -> Prelude.bool
val raw_associated_item :
Ast.attrs ->
(Hax_engine__Attr_payloads.AssocRole.T.t * Hax_engine__Attr_payloads.UId.T.t)
Prelude.list