Control.Relation.Closure

Definitions

data SymClosure : Rel ty -> ty -> ty -> Type

Totality: total
Visibility: public export
Constructors:

Fwd : rel x y -> SymClosure rel x y

Bwd : rel y x -> SymClosure rel x y

Hints:

Reflexive ty rel => Reflexive ty (SymClosure rel)

Symmetric ty (SymClosure rel)

data TransClosure : Rel ty -> ty -> ty -> Type

Totality: total
Visibility: public export
Constructors:

Nil : TransClosure rel x x

(::) : rel x y -> TransClosure rel y z -> TransClosure rel x z

Hints:

Symmetric ty rel => Equivalence ty (TransClosure rel)

Symmetric ty rel => Euclidean ty (TransClosure rel)

Symmetric ty rel => PartialEquivalence ty (TransClosure rel)

Reflexive ty (TransClosure rel)

Symmetric ty rel => Symmetric ty (TransClosure rel)

Symmetric ty rel => Tolerance ty (TransClosure rel)

Transitive ty (TransClosure rel)