WPropertiesOn (p.jasmin.2025.06.1.doc.jasmin.jasmin.Jasmin.MSetProperties.WPropertiesOn)

Parameters

module E : Equalities.DecidableType

module M : sig ... end

Signature

module Dec : sig ... end

module FM : sig ... end

val coq_In_dec : M.elt -> M.t -> bool

val of_list : M.elt list -> M.t

val to_list : M.t -> M.elt list

val fold_rec : 
  (M.elt -> 'a1 -> 'a1) ->
  'a1 ->
  M.t ->
  (M.t -> __ -> 'a2) ->
  (M.elt -> 'a1 -> M.t -> M.t -> __ -> __ -> __ -> 'a2 -> 'a2) ->
  'a2

val fold_rec_bis : 
  (M.elt -> 'a1 -> 'a1) ->
  'a1 ->
  M.t ->
  (M.t -> M.t -> 'a1 -> __ -> 'a2 -> 'a2) ->
  'a2 ->
  (M.elt -> 'a1 -> M.t -> __ -> __ -> 'a2 -> 'a2) ->
  'a2

val fold_rec_nodep : 
  (M.elt -> 'a1 -> 'a1) ->
  'a1 ->
  M.t ->
  'a2 ->
  (M.elt -> 'a1 -> __ -> 'a2 -> 'a2) ->
  'a2

val fold_rec_weak : 
  (M.elt -> 'a1 -> 'a1) ->
  'a1 ->
  (M.t -> M.t -> 'a1 -> __ -> 'a2 -> 'a2) ->
  'a2 ->
  (M.elt -> 'a1 -> M.t -> __ -> 'a2 -> 'a2) ->
  M.t ->
  'a2

val fold_rel : 
  (M.elt -> 'a1 -> 'a1) ->
  (M.elt -> 'a2 -> 'a2) ->
  'a1 ->
  'a2 ->
  M.t ->
  'a3 ->
  (M.elt -> 'a1 -> 'a2 -> __ -> 'a3 -> 'a3) ->
  'a3

val set_induction : 
  (M.t -> __ -> 'a1) ->
  (M.t -> M.t -> 'a1 -> M.elt -> __ -> __ -> 'a1) ->
  M.t ->
  'a1

val set_induction_bis : 
  (M.t -> M.t -> __ -> 'a1 -> 'a1) ->
  'a1 ->
  (M.elt -> M.t -> __ -> 'a1 -> 'a1) ->
  M.t ->
  'a1

val cardinal_inv_2 : M.t -> Datatypes.nat -> M.elt

val cardinal_inv_2b : M.t -> M.elt