Eric Wieser

@mdickinson, I see you recently reviewed some ctypes PRs; would you mind taking a quick look at this one?

Thanks for testing! Given this file has 52 asserts (11 on std_dict) and no `Py_FatalError`s, I'd be inclined to declare that change out of scope. Is that ok?

~~Oops, just realized that I probably clobbered the buildbot status by merging main; github was giving me a red cross so I clicked the update button without looking carefully enough...~~...

@mdickinson, I really appreciate that you were able to review #5576 a few weeks ago. Do you think you'd be able to take a look at this one too?

Yes, you're right; the cases that don't set `_pack_` at all are platform-dependent. I think a test written for 32 bit platforms would pass on both; so replacing the uint64...

Duplicate of #22

I'm afraid I probably have no time today to do so, but might later this week. My figuring is that this is very unlikely to break anything, since the change...

> 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 won't run until...

awaiting-review

@semorrison, do you think this is ok as is? While there's [some discussion above](https://github.com/leanprover/lean4/pull/3090#discussion_r1485204250) about instantiating metavariables, it's mainly about code that isn't part of this patch anyway; and the...