Syntax.PreorderReasoning

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

Definitions

data Step : 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: 

(...) : (0 y : a) -> (0 _ : x = y) -> Step x y

data FastDerivation : a -> b -> Type

Totality: total
Visibility: public export
Constructors:

(|~) : (0 x : a) -> FastDerivation x x

(~~) : FastDerivation x y -> Step y z -> FastDerivation x z

Calc : (0 _ : FastDerivation x y) -> x = y

Visibility: public export

(..<) : (0 y : a) -> (0 _ : y = x) -> Step x y

Visibility: public export
Fixity Declarations:
infix operator, level 1
infix operator, level 1

(..>) : (0 y : a) -> (0 _ : x = y) -> Step x y

Visibility: public export
Fixity Declarations:
infix operator, level 1
infix operator, level 1

(~=) : FastDerivation x y -> (0 z : dom) -> {auto 0 _ : y = z} -> FastDerivation x z

  Use a judgemental equality but is not trivial to the reader.

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