Idris2Doc : Syntax.PreorderReasoning.Generic

Syntax.PreorderReasoning.Generic

CalcWith : Preorderdomleq => FastDerivationleqxy -> leqxy
FastDerivation : (a -> a -> Type) -> a -> a -> Type
Totality: total
Constructors:
(|~) : (x : a) -> FastDerivationleqxx
(<~) : FastDerivationleqxy -> Stepleqyz -> FastDerivationleqxz
Step : (a -> a -> Type) -> a -> a -> Type
Totality: total
Constructor: 
(...) : (y : a) -> leqxy -> Stepleqxy
(~~) : FastDerivationleqxy -> StepEqualyz -> FastDerivationleqxz

Fixity Declaration: infixl operator, level 0