Syntax.PreorderReasoning.Setoid

Like Syntax.PreorderReasoning.Generic, but optimised for setoids

Definitions

data Step : (a : Setoid) -> U a -> U a -> Type

Totality: total
Visibility: public export
Constructor: 

(...) : (0 y : U a) -> (a .equivalence) .relation x y -> Step a x y

data FastDerivation : (a : Setoid) -> U a -> U a -> Type

Totality: total
Visibility: public export
Constructors:

(|~) : (x : U a) -> FastDerivation a x x

(~~) : FastDerivation a x y -> Step a y z -> FastDerivation a x z

CalcWith : (a : Setoid) -> FastDerivation a x y -> (a .equivalence) .relation x y

Visibility: public export

(..<) : (y : U a) -> (a .equivalence) .relation y x -> Step a x y

Visibility: public export
Fixity Declarations:
infix operator, level 1
infix operator, level 1
infix operator, level 1

(..>) : (0 y : U a) -> (a .equivalence) .relation x y -> Step a x y

Visibility: public export
Fixity Declarations:
infix operator, level 1
infix operator, level 1
infix operator, level 1

(.=.) : (y : U a) -> x = y -> Step a x y

Visibility: public export
Fixity Declarations:
infix operator, level 1
infix operator, level 1
infix operator, level 1

(.=>) : (y : U a) -> x = y -> Step a x y

Visibility: public export
Fixity Declarations:
infix operator, level 1
infix operator, level 1
infix operator, level 1

(.=<) : (y : U a) -> y = x -> Step a x y

Visibility: public export
Fixity Declarations:
infix operator, level 1
infix operator, level 1
infix operator, level 1