Idris2Doc : 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