Seppel3210

geez the code size will probably be huge with that as well :cold_sweat: @Amdahl-rs Instead of `type Item = dyn SomeTrait;` you maybe meant `type Item = Box`? Or if...

And also where is the `Scalar` trait defined? Is it in your crate or an external one? If it is external: which one?

Depends on some things. First of all: What operating System are you on?

BTW porting over the lemma from my std4 PR leanprover/std4#690 was pretty easy: https://github.com/Seppel3210/std4/commit/109c3ce97e182813a166c9b55418d9a599a01bb6 So this is definitely bug free :smile: I also think this makes the API nicer

awaiting-review

Oops 🤦 Linter errors should be fixed now

as I said on the other PR @timotree3: In the case that your PR gets merged (and std4's lean-toolchain gets bumped) I have a commit lying around that fixes the...

I think it makes sense to wait for the lean4 version to get bumped since the lean4 PR was merged. Or should I PR it to the bump branch instead?...

hmm, the linter fail seems to be an issue with derive_functional_induction. The `this` it's referring to is the ignored argument in `case1`

Not really sure who to ping for this issue :sweat_smile: @semorrison