Andres Erbsen

I think that's a part of it, but there was already an entry for the right jabber id on what I thought was a list of contacts, which I needed...

This indeed seems better now. The following works too: ```coq Module Foo. Reserved Notation "x --> y" (at level 55). Notation "x --> y" := (x+y) (at level 55). Check...

Some work was done and I am unsure how far it got; I am following up with the implementers.

Yes, https://github.com/Matir03/fiat-crypto/commits/master now contains what was done.

https://github.com/Yawning/secp256k1-voi https://github.com/mit-plv/fiat-crypto/issues/1444#issuecomment-1580900399

Do you really want to maintain this, though? I would much rather spend my time learning how to statically link ocaml than dealing with docker and deployment automation.

I believe the version at http://bitmath.blogspot.com/2012/09/calculating-lower-bound-of-bitwise-or.html is supposed to be tight. It is credited back to Hacker's Delight anyway. I wonder whether porting it might give a better Coq function.

We in fact do integrate primality proofs now

``` 2 | opam exec -- cat ~/.opam/log/* | ~~~~ | The term 'opam' is not recognized as a name of a cmdlet, function, script file, or executable program. Check...

https://github.com/mit-plv/bedrock2/actions/runs/3653687403/jobs/6176913824 timed out for no reason I can see