Andres Erbsen

Are you suggesting we'd also take PRs straight to `tested`? If not, I don't think this satisfies @proux01's request.

The way the Bedrock2 maintainers have chosen to manage their CI is to not test against users and instead perform catch-up for non-backwards-compatible changes when bumping the bedrock2 submodule in...

> Well, I certainly understand it feels simpler from your point of view since it transfers, at least part of, the complexity on our side. That's exactly what we are...

I have been working towards reducing reliance on `Vector`, but I am not sure whether it should be removed or even deprecated. For example, I hear vector is preferable for...

I would be very happy to have the documentation of this module give a down-to-earth overview of the considerations for why one might not want to use it, both based...

coqutil tuples do not use typeclasses or any other programmable elaboration. I am not attached to the specific definition in coqutil and would be happy to work on standardization without...

@herbelin there are a few developments using recursive formulations, see [fiat-crypto tuples](https://github.com/mit-plv/fiat-crypto/blob/85e08224eca3ce48f90a641bbf602769ccae3629/src/Util/Tuple.v#L258), [kami Vec and Fin](https://github.com/sifive/Kami/blob/ffb77238f27b603dbd42d2622ba911740bf5eadf/Simulator/CoqSim/Misc.v#L4-L16), [color prodn](https://github.com/fblanqui/color/blob/5edcc649fc0b4a644ef38b722103954eee706bac/Util/Relation/Lexico.v#L113), [coqutil tuples](https://github.com/mit-plv/coqutil/blob/63991a44767767565e7785cab1a70abe2af90e5c/src/coqutil/Datatypes/HList.v#L84). IMO they work fine, as do the ones based on...

> I see, so, a development of functions on tuples would still need to be done iiuc. The coqutil tuple library is very light because we use it almost exclusively...

I think it would be great to have proof of this idea in the standard library, but I wonder about the specific statement. I would prefer a BoolSpec instance that...

I would be fine with having all of these; just IMO BoolSpec is the appropriately most general one. I am not sure whether we want the `pointwise_bounded_dec_ex_dec` at all as...