Joachim Breitner
Joachim Breitner
Is this really specific to instances, or can you reproduce it using normal definitions? The intended design is that the equational theorems are visible whenever the body of the corresponding...
`Int.reducetoInt` is a simproc using `Int8.toInt`. Have you tried adding `@[expose]` to `def Int8.toInt (i : Int8) : Int := i.toBitVec.toInt`?
May be fallout from https://github.com/leanprover/lean4/pull/10508 Realizable constants for decls from other modules and `MapDeclarationExtension` don't seem to match.
Strange, I cannot reproduce by copying the content of `src/Init/Data/List/OfFn.lean` into a test file in `tests/lean/run`.
Possible cause: Does the realizing code not check if the things does already exist. Maybe missing `withoutExporting`.
Most likely culprit: https://github.com/leanprover/lean4/pull/8096
PR #10425 is an attempt to fix this at least for discriminants that are proofs, maybe good enough to unblock #10268.
It may be possible to push further on this if `split`, when it’s generalizing a discriminant that’s dependent, fixes the type up by wrapping the `match` statement in something like...
> The replica actually use the presence of this caniser method to detect motoko canisters and other tooling might too (icrocks?). Perhaps 1. is a better solution. Sounds like a...
Right! with the async helper, I wouldn't hesitate to change the name. For the candid one, you are absolutely right.