Idris2Doc : Syntax.PreorderReasoning

Syntax.PreorderReasoning

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

Calc : FastDerivation x y -> x = y

data FastDerivation : a -> b -> Type

Totality: total
Constructors:

(|~) : (0 x : a) -> FastDerivation x x
(~~) : FastDerivation x y -> Step y z -> FastDerivation x z

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
Constructor:

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