Jason Gross

Why not? Or why not both, for the standard library at least?

> one standard way to reduce the size is to replace part of these conditions with computational checks, i.e. like for reflexive tactics. Isn't this effectively saying "the proof engine...

Would you say the same about intrinsically-typed representations of syntax? And more generally any recursive inductive type with indices?

> I see. But in my real-world application, which is Iris, the "typing judgement" is not inductively defined. I have a semantic definition of it, and a bunch of lemmas...

@fpottier See https://github.com/mit-plv/fiat-crypto/commit/93398f3889a094cc1862f8cad2d23f5661c4f852 in particular `reflect_wffT` and https://github.com/mit-plv/fiat-crypto/commit/71253e65b115f6332c544476bfe680a8d3f18568 which adds a great deal of documentation and exposition to the relevant file. This example does not include the CPS compression. Another...

> (I guess maybe I should have turned this into a functional pearl or at least written it up somewhere?) I guess I did actually write this up in [my...

> Why is the second representation more efficient? The first representation suffers quadratic overhead if you build conjunctions by `repeat constructor` and in proofs of `List.In`, which is encoded as...

Oh, huh, I guess it does, and that bit of my dissertation was wrong. I wonder if there's a way to issue a correction to it. I guess there is...

@ejgallego I've found that most of the time my cores are saturated on file-level parallelism, and haven't tried async-proofs much, alas. @andres-erbsen do you know if it speeds up the...

`par:` is crippled by its inability to share a jobserver with `make` (https://github.com/coq/coq/issues/14203), which means that we can't really take full advantage of it. Its also so memory-heavy/duplicative that we...