~jgross-h/coq/+git/coq:master

Branch merges

Related source package recipes

2 recipes using this branch. (?)

Create packaging recipe

Related snap packages

Related charm recipes

8e5377c... by "coqbot-app[bot]" <50967743+coqbot-app[bot]@users.noreply.github.com> 4 hours ago

Merge PR #18628: More bitwise in Numbers.Natural.Abstract

Reviewed-by: andres-erbsen
Ack-by: proux01
Co-authored-by: andres-erbsen <email address hidden>

a393f28... by Andres Erbsen <email address hidden> on 2024-04-15

changelog, a missing lemma, and test

87ef36a... by "coqbot-app[bot]" <50967743+coqbot-app[bot]@users.noreply.github.com> 14 hours ago

Merge PR #18979: Enter `Hint Extern` patterns syntactically into the Bnet

Reviewed-by: ppedrot
Co-authored-by: ppedrot <email address hidden>

d2c1874... by Pierre Rousselin <email address hidden> on 2024-02-15

Specialize new induction lemmas in implementations

The lemmas `strong_induction_le` and `binary_induction` in
`Numbers.Natural` are now marked as `Private_` and hidden from the
documentation.

Specialized versions (not hidden) are provided for `PeanoNat` and (only
`strong_induction`) for `BinNat`.

A new test file for these induction lemmas (and other additions in #18628)
is provided.

59c5442... by Pierre Rousselin <email address hidden> on 2024-02-13

Move a part of PeanoNat to Natural

There is still an issue with `div2_double` and `div2_succ_double`.
It's not possible to factor these because there are different such
lemmas in `PeanoNat` and `BinNat`.
So we settle for `div2_even` and `div2_odd'` in `NBits`.
`div2_even` will appear twice (the other name is `div2_double`) in
`PeanoNat`. Maybe this is not a big problem?

The naming convention in Numbers is now (mostly) that
- `even` after an operation name means (2 * n)
- `odd` after an operation name means (2 * n + 1)
- `even` as a prefix means it is about the boolean operation `even`
- `same` for `odd`

Unfortunately this clashes with `div2_odd`, hence the name `div2_odd'`.

There are still some questions about the `div2` inequalities (some new
in `NBits`, some imported from `PeanoNat`); some of which are very
similar.

3bcefe9... by Pierre Rousselin <email address hidden> on 2024-02-10

Add lt_div2_diag_l in NBits

051bb65... by Pierre Rousselin <email address hidden> on 2024-02-08

Simplify proofs and add missing lemmas in Natural

9da39dc... by Pierre Rousselin <email address hidden> on 2024-02-06

Renamings in Nbits and div2_(lower|upper)_bound

Also removed some parentheses around function applications when it's
clearer to read.

37c7595... by Pierre Rousselin <email address hidden> on 2024-02-05

Add ones_zero and ones_succ

6617f95... by Pierre Rousselin <email address hidden> on 2024-02-04

Add shiftr_le le_shiftl and le_div2_diag_l

TODO: Not sure about the names for shift and le names.