Syntax.PreorderReasoning.Generic

Definitions

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

Totality: total
Visibility: public export
Constructor: 

(...) : (y : a) -> leq x y -> Step leq x y

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

Totality: total
Visibility: public export
Constructors:

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

(<~) : FastDerivation leq x y -> Step leq y z -> FastDerivation leq x z

CalcWith : Preorder dom leq => FastDerivation leq x y -> leq x y

Visibility: public export

(~~) : FastDerivation leq x y -> Step Equal y z -> FastDerivation leq x z

Visibility: public export
Fixity Declaration: infixl operator, level 0

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

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

(..>) : (y : a) -> leq x y -> Step leq x y

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

(.=.) : Reflexive a leq => (y : a) -> x = y -> Step leq x y

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

(.=>) : Reflexive a leq => (y : a) -> x = y -> Step leq x y

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

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

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