!4#3187 (Data.Seq.Seq)

Stream: mathlib4

[Arien Malec]

Have this down to two issues, documented in the PR notes -- would appreciate extra pairs of eyes on these, because there's something I'm missing here. Otherwise cleaned up.

[Eric Wieser]

documented in the PR notes

I don't know what you mean by the PR notes, but the PR description is empty.

[Arien Malec]

PR comment rather than the PR field itself...

[Arien Malec]

I saw your note on recOn but here we are recursing on destruct s (Option (Seq1 \alpha)) rather than on Seq itself...

Is there a clean way to get the H in induction' H: destruct s using match?

[Eric Wieser]

What's the error you get when you remove non-computable?

[Eric Wieser]

I don't think you need to switch to using a match, this sounds like an #xy problem

[Arien Malec]

code generator does not support recursor 'Option.rec' yet, consider using 'match ... with' and/or structural recursion

[Arien Malec]

Switching to cases' from induction' fixed the issue (we don't use an induction hypothesis anyway).

[Eric Wieser]

Adding Option.rec_eq_recC would fix that

[Eric Wieser]

(c.f. docs4#List.rec_eq_recC)

[Arien Malec]

Let me take a crack at a PR for that -- I saw the pattern for List...

[Arien Malec]

I think !4#3255 is what's required, but would appreciate review.

[Arien Malec]

Just tested it in situ in Data.Seq.Seq and does the job.

[Arien Malec]

(modulo simp to csimp)