WithItems (hax-engine.Hax_engine.Backend.Make.Attrs.WithItems)

Parameters

module I : sig ... end

Signature

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 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 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