Joachim Breitner

Yes, also curious for a good idiom about reporting such error messages, e.g. for ``` do n

Why? If this is not the bottle neck (and it is not, as we are downloading large json files anyways), then having all from one source is more reliable. Also...

> Without a CDN, install-jslibs.sh would have to be embedded. Or alternatively, it has to be run at compile time and the resulting files embedded.

> So perhaps it's not worth the bother if the whole thing is going to be deprecated anyway. We still need a proposal to allow this in the new report,...

I did now include the GHC doc as the detailed description.

Good point. I hope that `ScopedTypeVariables` will also be a default in a future standard :-) Is there anything reasonable we can do to improve this corner case?

> > It would be good to have a Mathlib build for this one. Could you rebase onto `nightly-with-mathlib`? > > I did this rebase @semorrison, but I guess CI...

Seems to work (https://github.com/leanprover/lean4/actions/runs/7274620683/job/19820906002), mathlib CI should be running

A modifier that produces truely large `Integer` and `Natural` values would be good; I am testing an encoding library right now. I ended up using this code, inspired by @arybczak...

But in that case, the `vec null` wouldn't be decoded to a huge value, would it? The subtype check would run first, and just return `null`? The code that then...