* Emit warning for fixities with no export modifiers
This is to help update all the existing code to program with explicit
fixity export directives in preparation for the behavioral change where
they will become private by default.
Refactor the DIY equational reasoning library to be a bit more like
the generic pre-order reasoning library:
Change the `...` notation into a constructor for a new `Step` datatype.
This seems to help idris disambiguate between the two kinds of
reasoning when they're used in the same file (e.g., frex).
Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
Division Theorem. For every natural number `x` and positive natural
number `n`, there is a unique decomposition:
`x = q*n + r`
with `q`,`r` natural and `r` < `n`.
`q` is the quotient when dividing `x` by `n`
`r` is the remainder when dividing `x` by `n`.
This commit adds a proof for this fact, in case
we want to reason about modular arithmetic (for example, when dealing
with binary representations). A future, more systematic, development could
perhaps follow: @clayrat 's (idris1) port of Coq's binary arithmetics:
https://github.com/sbp/idris-bi/blob/master/src/Data/Bin/DivMod.idrhttps://github.com/sbp/idris-bi/blob/master/src/Data/Biz/DivMod.idrhttps://github.com/sbp/idris-bi/blob/master/src/Data/BizMod2/DivMod.idr
In the process, it bulks up the stdlib with:
+ a generic PreorderReasoning module for arbitrary preorders,
analogous for the equational reasoning module
+ some missing facts about Nat operations.
+ Refactor some Nat order properties using a 'reflect' function
Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
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
