sibylfs-lem 0.4.0 (latest)

type (!'a, !'b) rel_pred = 'a -> 'b -> bool

type ('a, 'b) rel_set = ('a * 'b) Pset.set

type ('a, 'b) rel = ('a, 'b) rel_set

val relEq : 'a -> 'b -> 'c Pset.set -> 'c Pset.set -> bool

val relToPred : 'a -> 'b -> 'c -> 'd -> ('e * 'f) Pset.set -> 'e -> 'f -> bool

val relFromPred : 
  'a Lem_basic_classes.setType_class ->
  'b Lem_basic_classes.setType_class ->
  'c ->
  'd ->
  'a Pset.set ->
  'b Pset.set ->
  ('a -> 'b -> bool) ->
  ('a * 'b) Pset.set

val relIdOn : 
  'a Lem_basic_classes.setType_class ->
  'a Lem_basic_classes.eq_class ->
  'a Pset.set ->
  ('a * 'a) Pset.set

val relComp : 
  'a Lem_basic_classes.setType_class ->
  'b ->
  'c Lem_basic_classes.setType_class ->
  'd ->
  'e Lem_basic_classes.eq_class ->
  ('a * 'e) Pset.set ->
  ('e * 'c) Pset.set ->
  ('a * 'c) Pset.set

val relRestrict : 
  'a Lem_basic_classes.setType_class ->
  'b ->
  ('a * 'a) Pset.set ->
  'a Pset.set ->
  ('a * 'a) Pset.set

val relConverse : 
  'a Lem_basic_classes.setType_class ->
  'b Lem_basic_classes.setType_class ->
  ('a * 'b) Pset.set ->
  ('b * 'a) Pset.set

val relDomain : 
  'a Lem_basic_classes.setType_class ->
  'b ->
  ('a * 'c) Pset.set ->
  'a Pset.set

val relRange : 
  'a ->
  'b Lem_basic_classes.setType_class ->
  ('c * 'b) Pset.set ->
  'b Pset.set

val relOver : 
  'a Lem_basic_classes.setType_class ->
  ('a * 'a) Pset.set ->
  'a Pset.set ->
  bool

val relApply : 
  'a ->
  'b Lem_basic_classes.setType_class ->
  'c ->
  ('d * 'b) Pset.set ->
  'd Pset.set ->
  'b Pset.set

val isReflexiveOn : 'a -> 'b -> ('c * 'c) Pset.set -> 'c Pset.set -> bool

val isIrreflexiveOn : 'a -> 'b -> ('c * 'c) Pset.set -> 'c Pset.set -> bool

val isIrreflexive : 
  'a ->
  'b Lem_basic_classes.eq_class ->
  ('b * 'b) Pset.set ->
  bool

val isSymmetricOn : 'a -> 'b -> ('c * 'c) Pset.set -> 'c Pset.set -> bool

val isSymmetric : 'a -> 'b -> ('c * 'c) Pset.set -> bool

val isAntisymmetricOn : 
  'a ->
  'b Lem_basic_classes.eq_class ->
  ('b * 'b) Pset.set ->
  'b Pset.set ->
  bool

val isAntisymmetric : 
  'a ->
  'b Lem_basic_classes.eq_class ->
  ('b * 'b) Pset.set ->
  bool

val isTransitiveOn : 'a -> 'b -> ('c * 'c) Pset.set -> 'c Pset.set -> bool

val isTransitive : 
  'a Lem_basic_classes.setType_class ->
  'b ->
  ('a * 'a) Pset.set ->
  bool

val isTotalOn : 'a -> 'b -> ('c * 'c) Pset.set -> 'c Pset.set -> bool

val isTrichotomousOn : 
  'a ->
  'b Lem_basic_classes.eq_class ->
  ('b * 'b) Pset.set ->
  'b Pset.set ->
  bool

val isSingleValued : 
  'a Lem_basic_classes.setType_class ->
  'b Lem_basic_classes.setType_class ->
  'c ->
  'b Lem_basic_classes.eq_class ->
  ('a * 'b) Pset.set ->
  bool

val isEquivalenceOn : 'a -> 'b -> ('c * 'c) Pset.set -> 'c Pset.set -> bool

val isPreorderOn : 'a -> 'b -> ('c * 'c) Pset.set -> 'c Pset.set -> bool

val isPartialOrderOn : 
  'a ->
  'b Lem_basic_classes.eq_class ->
  ('b * 'b) Pset.set ->
  'b Pset.set ->
  bool

val isStrictPartialOrderOn : 
  'a ->
  'b ->
  ('c * 'c) Pset.set ->
  'c Pset.set ->
  bool

val isStrictPartialOrder : 
  'a Lem_basic_classes.setType_class ->
  'a Lem_basic_classes.eq_class ->
  ('a * 'a) Pset.set ->
  bool

val isTotalOrderOn : 
  'a ->
  'b Lem_basic_classes.eq_class ->
  ('b * 'b) Pset.set ->
  'b Pset.set ->
  bool

val isStrictTotalOrderOn : 
  'a ->
  'b Lem_basic_classes.eq_class ->
  ('b * 'b) Pset.set ->
  'b Pset.set ->
  bool

val transitiveClosureAdd : 
  'a Lem_basic_classes.setType_class ->
  'b ->
  'a ->
  'a ->
  ('a * 'a) Pset.set ->
  ('a * 'a) Pset.set

val reflexivTransitiveClosureOn : 
  'a Lem_basic_classes.setType_class ->
  'a Lem_basic_classes.eq_class ->
  ('a * 'a) Pset.set ->
  'a Pset.set ->
  ('a * 'a) Pset.set

package sibylfs-lem