Why is `Mathlib.ModelTheory.Encoding` using `SizeOf.sizeOf`?

Stream: mathlib4

[Kim Morrison]

@Aaron Anderson or others who know about file#ModelTheory/Encoding, why is listDecode written in terms of SizeOf.sizeOf?

Generally, this is meant to be an "implementation detail", rather than used in mathematical proofs.

If there is some good explanation for it here, I'd like to have this documented.

Alternatively, can we just use List.length here? What is going on?

[Joachim Breitner]

I assume this is because listDecode is recursive and calls itself on itself ((listDecode (listDecode l).2), so you need the subtype to indicate that the result is smaller than the input. It seems that subsequent definitions only use (listDecode l).1 anyways.
But I suppose with termination_by l => l.length using length would work just as well, as you say.

[Aaron Anderson]

Essentially, because I had trouble proving well-founded recursion. I've just attempted to retrofit it to use List.length, and found that `termination_by l => l.length' didn't work automatically. I'll try to make it work, but perhaps just changing the encoding (to use parentheses, say) would be easier.

[Aaron Anderson]

I've changed the decoding a bit, and now List.length works. #15209

[Aaron Anderson]

I think it makes more sense - I could try to make it even clearer, but I think it's best for me to PR this now to remove all the deprecated stuff, and tinker more later.

[Kim Morrison]

Thanks!