Jason Gross

```coq Theorem foobar : 1=1. reflexivity. Defined. Opaque foobar. Hint Transparent foobar : plus. Hint Extern 1 => idtac "unfold"; unfold foobar; idtac "after" : plus. Goal foobar = foobar....

That said, it's not entirely clear to me why `Transparent` (and `Strategy` more generally) cannot be subsumed by `Hint Transparent` on some default database.

> Would you be willing to try and find an example showing that `Hint Transparent/Opaque` does anything? What should it do? Is that valuable? I don't have time right now,...

Assuming we want to match https://boringssl.googlesource.com/boringssl/+/aa31748bc84f0cd499e4b0337bf929b132aab1cc, we could add a `--msvc` flag that enables an adjustment to https://github.com/mit-plv/fiat-crypto/blob/457cb5e1147fa865bb168f073d3028563e364a38/src/Stringification/C.v#L116-L166 to include ``` #include #if defined(_M_X64) #include #endif ``` and emits the...

Hm, but it's not entirely clear how this should be structured. Maybe we should add support for each backend to describe a collection of "here's the string body of this...

> Would it be feasible to generate a mashup of secp256k1 C that uses functions like `u128_mul`, `u128_add` instead of operators on the native type? This should be pretty easy...

No, I haven't had a chance to work on this, and don't expect to have time soon. @andres-erbsen are you working on this?

> No, and I don't understand your suggestion. What does `Z.add_modulo` have to do with it? Probably `Z.add_modulo` is wrong, and I should have written `Z.add_carry_full` or whatever

I ended up using the following, which I guess works well enough ```latex \makeatletter \NewDocumentCommand{\NumAsPow}{oO{2}m}{\ensuremath{% \edef\NumAsPow@exp{\fpeval{ln(#3)/ln(#2)}}% \edef\NumAsPow@expf{\fpeval{floor(\NumAsPow@exp)}}% \edef\NumAsPow@mantissa{\fpeval{(#3)/(#2^{\NumAsPow@expf})}}% \IfNoValueTF{#1}{% #2^{\num[round-precision=0,round-mode=places]{\NumAsPow@exp}}% }{% \num[exponent-base=#2,#1]{\NumAsPow@mantissa e\NumAsPow@expf}% }% }} \makeatother ```