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 : (0_ : FastDerivationxy) ->x=y
Visibility: public export
(..<) : (0y : a) -> (0_ : y=x) ->Stepxy
Visibility: public export
Fixity Declarations:
infix operator, level 1
infix operator, level 1
(..>) : (0y : a) -> (0_ : x=y) ->Stepxy
Visibility: public export
Fixity Declarations:
infix operator, level 1
infix operator, level 1
(~=) : FastDerivationxy-> (0z : dom) -> {auto0_ : y=z} ->FastDerivationxz
  Use a judgemental equality but is not trivial to the reader.

Visibility: public export
Fixity Declarations:
infixl operator, level 0
infixl operator, level 0