sizeOf noncomputable

Stream: lean4

[Jakob von Raumer]

Is it intended that automatically derived SizeOf instances are generally noncomputable?

[Edward van de Meent]

It wouldn't surprise me, the purpose of the class is to help with termination proofs, and I think those get erased by the code generator

[Edward van de Meent]

So the implementation doesn't need it to be computable

[Jakob von Raumer]

Okay, yes I guess that makes sense.

[Jakob von Raumer]

Follow-up question: Why is the generated SizeOf instance not more like constructorIdx + noOfConstructors*depth instead of just depth?

[Henrik Böving]

That feels like a very good chance for brittleness as it imposes an implicit ordering on the constructors so whenver an inductive just changes its order of ctors there is potential for termination proofs to fail

[Jakob von Raumer]

Could also have it as an opt-in option in that case

[Henrik Böving]

If you want to do custom sizeOf with these properties that you can execute you can just override the instance btw, in case that is the actual motivation here

[Jakob von Raumer]

We do that manually for an enum of 48 constructors or so that's generated from Sail, but maybe I'll just give myself the task of automating the construction and writing a deriver for this

[Jakob von Raumer]

(Would that be of interest to Lean core?)