Alex Gryzlov
Alex Gryzlov
This looks relevant: https://github.com/AbsInt/CompCert/blob/master/lib/Integers.v
https://github.com/maximedenes/native-coq/tree/master/theories/Numbers also looks fitting
As well as https://github.com/artart78/coq-bits It even has an accompanying paper https://pages.lip6.fr/Pierre-Evariste.Dagand/stuffs/coq-bitset/flops/paper.pdf
- Use sections more, e.g. `(bizMult 2)` -> `(2*)` (esp now that https://github.com/idris-lang/Idris-dev/pull/4119 is merged) - Look for places where two `rewrite`s/`replace`s can be rolled into `trans`
Order of multiplication in the divMod-style proofs: in some places it's `b*q+r`, in others it's `q*b+r`; would be nice to choose a single style (personally I like `q*b+r` more) to...
Introduce lemmas to do rewrites like `a 'compare' (b+c) = (a-c) 'compare' b` directly, without `addAssoc` and `posSubDiag`
Try to simplify `*Spec` types by removing explicit equalities ala: ``` %default total data NatM = NatO | NatP Nat | NatN data NatMSpec : (p, q : Nat) ->...
Try wrapping `signed` (and `unsigned`?) in records to prevent over-normalization a-la `Box` in https://gallais.github.io/pdf/agdarsec17.pdf
This will also help to do https://github.com/sbp/idris-bi/issues/8 as the functions mentioned reference `Bin`.
Yeah, makes sense.