Mmake (p.jasmin.2025.06.1.doc.jasmin.jasmin.Jasmin.Gen

Parameters

module K' : CmpType

Signature

module K : sig ... end

module Ordered : sig ... end

module Map : sig ... end

module Facts : sig ... end

type 't t = 't Map.t

val empty : 'a1 t

val is_empty : 'a1 t -> bool

val get : 'a1 t -> Eqtype.Equality.sort -> 'a1 option

val set : 'a1 t -> Eqtype.Equality.sort -> 'a1 -> 'a1 Map.t

val remove : 'a1 t -> Eqtype.Equality.sort -> 'a1 Map.t

val map : ('a1 -> 'a2) -> 'a1 Map.t -> 'a2 Map.t

val mapi : (Map.key -> 'a1 -> 'a2) -> 'a1 Map.t -> 'a2 Map.t

val raw_map2 : 
  (Eqtype.Equality.sort -> 'a1 option -> 'a2 option -> 'a3 option) ->
  'a1 Map.Raw.tree ->
  'a2 Map.Raw.tree ->
  'a3 Map.Raw.tree

val elements : 'a1 Map.t -> (Map.key * 'a1) list

val fold : (Map.key -> 'a1 -> 'a2 -> 'a2) -> 'a1 Map.t -> 'a2 -> 'a2

val all_t : (Eqtype.Equality.sort -> 'a1 -> bool) -> 'a1 Map.Raw.tree -> bool

val has_t : (Eqtype.Equality.sort -> 'a1 -> bool) -> 'a1 Map.Raw.tree -> bool

val incl_t : 
  (Eqtype.Equality.sort -> 'a1 -> bool) ->
  (Eqtype.Equality.sort -> 'a1 -> 'a2 -> bool) ->
  'a1 Map.Raw.tree ->
  'a2 Map.Raw.tree ->
  bool

val all : (Eqtype.Equality.sort -> 'a1 -> bool) -> 'a1 t -> bool

val has : (Eqtype.Equality.sort -> 'a1 -> bool) -> 'a1 t -> bool

val incl_def : 
  (Eqtype.Equality.sort -> 'a1 -> bool) ->
  (Eqtype.Equality.sort -> 'a1 -> 'a2 -> bool) ->
  'a1 Map.bst ->
  'a2 Map.bst ->
  bool

val incl : 
  (Eqtype.Equality.sort -> 'a1 -> 'a2 -> bool) ->
  'a1 Map.bst ->
  'a2 Map.bst ->
  bool

val in_codom : 
  Eqtype.Equality.coq_type ->
  Eqtype.Equality.sort ->
  Eqtype.Equality.sort t ->
  bool

val map2 : 
  (Eqtype.Equality.sort -> 'a1 option -> 'a2 option -> 'a3 option) ->
  'a1 t ->
  'a2 t ->
  'a3 t

val filter_map : (Eqtype.Equality.sort -> 'a1 -> 'a2 option) -> 'a1 t -> 'a2 t

val is_emptyP : 'a1 t -> Bool.reflect

val elementsP : 
  Eqtype.Equality.coq_type ->
  (Eqtype.Equality.sort * Eqtype.Equality.sort) ->
  Eqtype.Equality.sort t ->
  Bool.reflect