Idris2Doc : Syntax.PreorderReasoning

Syntax.PreorderReasoning

Until Idris2 starts supporting the 'syntax' keyword, here's a
poor-man's equational reasoning

Definitions

dataStep : a->b->Type
  Slightly nicer syntax for justifying equations:
```
|~ a
~~ b ...( justification )
```
and we can think of the `...( justification )` as ASCII art for a thought bubble.

Totality: total
Visibility: public export
Constructor: 
(...) : (0y : a) -> (0_ : x=y) ->Stepxy
dataFastDerivation : a->b->Type
Totality: total
Visibility: public export
Constructors:
(|~) : (0x : a) ->FastDerivationxx
(~~) : FastDerivationxy->Stepyz->FastDerivationxz
Calc : FastDerivationxy->x=y
Visibility: public export
symHet : (0_ : x=y) ->y=x
Visibility: public export
(..<) : (0y : a) ->y=x->Stepxy
Visibility: public export
Fixity Declaration: infix operator, level 1
(..>) : (0y : a) -> (0_ : x=y) ->Stepxy
Visibility: public export
Fixity Declaration: infix operator, level 1