Idris2Doc : Syntax.PreorderReasoning

Syntax.PreorderReasoning

Calc : FastDerivationxy -> x = y
FastDerivation : a -> b -> Type
Totality: total
Constructors:
(|~) : (0 x : a) -> FastDerivationxx
(~~) : FastDerivationxy -> Stepyz -> FastDerivationxz
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) -> Stepxy