mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 00:31:57 +03:00
d82a3e0e42
For lack of a better place, I've put it in `Syntax.PreorderReasoning` These equations are natural in equational reasoning, but less so when rewriting, so that's why it's there |
||
---|---|---|
.. | ||
PreorderReasoning.idr | ||
WithProof.idr |