Idris2Doc : Syntax.PreorderReasoning.Generic

Syntax.PreorderReasoning.Generic

CalcWith : Preorder dom leq => FastDerivation leq x y -> leq x y
  
data FastDerivation : (a -> a -> Type) -> a -> a -> Type
  Totality: total
  Constructors:
  
(|~) : (x : a) -> FastDerivation leq x x
  
(<~) : FastDerivation leq x y -> Step leq y z -> FastDerivation leq x z
data Step : (a -> a -> Type) -> a -> a -> Type
  Totality: total
  Constructor: 
(...) : (y : a) -> leq x y -> Step leq x y
(~~) : FastDerivation leq x y -> Step Equal y z -> FastDerivation leq x z
  
  Fixity Declaration: infixl operator, level 0