WithItems (hax-engine.Fstar_backend.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 : 
  Hax_engine.Ast.attrs ->
  (Hax_engine__Attr_payloads.AssocRole.T.t,
    AST.item Hax_engine.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 ->
  Hax_engine.Ast.attrs ->
  AST.item Hax_engine.Prelude.option

val associated_fn : 
  Hax_engine__Attr_payloads.AssocRole.T.t ->
  Hax_engine.Ast.attrs ->
  (AST.generics * AST.param Hax_engine.Prelude.list * AST.expr)
    Hax_engine.Prelude.option

val associated_expr : 
  ?keep_last_args:Hax_engine.Prelude.int ->
  Hax_engine__Attr_payloads.AssocRole.T.t ->
  Hax_engine.Ast.attrs ->
  AST.expr Hax_engine.Prelude.option

val associated_items : 
  Hax_engine__Attr_payloads.AssocRole.T.t ->
  Hax_engine.Ast.attrs ->
  AST.item Hax_engine.Prelude.list

val associated_fns : 
  Hax_engine__Attr_payloads.AssocRole.T.t ->
  Hax_engine.Ast.attrs ->
  (AST.generics * AST.param Hax_engine.Prelude.list * AST.expr)
    Hax_engine.Prelude.list

val associated_exprs : 
  ?keep_last_args:Hax_engine.Prelude.int ->
  Hax_engine__Attr_payloads.AssocRole.T.t ->
  Hax_engine.Ast.attrs ->
  AST.expr Hax_engine.Prelude.list

val expect_fn : 
  AST.item ->
  AST.generics * AST.param Hax_engine.Prelude.list * AST.expr

val expect_expr : 
  ?keep_last_args:Hax_engine.Prelude.int ->
  (AST.generics * AST.param Hax_engine.Prelude.list * AST.expr) ->
  AST.expr

val associated_refinement_in_type : 
  Hax_engine.Ast.span ->
  Hax_engine.Prelude.string Hax_engine.Prelude.list ->
  Hax_engine.Ast.attrs ->
  AST.expr Hax_engine.Prelude.option

val find_unique_attr : 
  Hax_engine.Ast.attrs ->
  f:(Hax_engine.Types.ha_payload -> 'a Hax_engine.Prelude.option) ->
  'a Hax_engine.Prelude.option

val status : Hax_engine.Ast.attrs -> Hax_engine.Types.ha_item_status

val late_skip : Hax_engine.Ast.attrs -> Hax_engine.Prelude.bool

val uid : 
  Hax_engine.Ast.attrs ->
  Hax_engine__Attr_payloads.UId.T.t Hax_engine.Prelude.option

val lemma : Hax_engine.Ast.attrs -> Hax_engine.Prelude.bool

val raw_associated_item : 
  Hax_engine.Ast.attrs ->
  (Hax_engine__Attr_payloads.AssocRole.T.t * Hax_engine__Attr_payloads.UId.T.t)
    Hax_engine.Prelude.list