Idris2Doc : Syntax.PreorderReasoning.Generic

Syntax.PreorderReasoning.Generic

Definitions

dataStep : (a->a->Type) ->a->a->Type
Totality: total
Visibility: public export
Constructor: 
(...) : (y : a) ->leqxy->Stepleqxy
dataFastDerivation : (a->a->Type) ->a->a->Type
Totality: total
Visibility: public export
Constructors:
(|~) : (x : a) ->FastDerivationleqxx
(<~) : FastDerivationleqxy->Stepleqyz->FastDerivationleqxz
CalcWith : Preorderdomleq=>FastDerivationleqxy->leqxy
Visibility: public export
(~~) : FastDerivationleqxy->StepEqualyz->FastDerivationleqxz
Visibility: public export
Fixity Declaration: infixl operator, level 0
(..<) : Symmetricaleq=> (y : a) ->leqyx->Stepleqxy
Visibility: public export
Fixity Declaration: infix operator, level 1
(..>) : (y : a) ->leqxy->Stepleqxy
Visibility: public export
Fixity Declaration: infix operator, level 1
(.=.) : Reflexivealeq=> (y : a) ->x=y->Stepleqxy
Visibility: public export
Fixity Declaration: infix operator, level 1
(.=>) : Reflexivealeq=> (y : a) ->x=y->Stepleqxy
Visibility: public export
Fixity Declaration: infix operator, level 1
(.=<) : Reflexivealeq=> (y : a) ->y=x->Stepleqxy
Visibility: public export
Fixity Declaration: infix operator, level 1