Create a "sizeOf" function with name declName using the recursor recName.
Instances For
Create sizeOf functions for all inductive datatypes in the mutual inductive declaration containing typeName
The resulting array contains the generated functions names. The NameMap maps recursor names into the generated function names.
There is a function for each element of the mutual inductive declaration, and for auxiliary recursors for nested inductive types.
Instances For
Instances For
SizeOf spec theorem for nested inductive types #
- indInfo : Lean.InductiveVal
- ctorName : Lake.Name
- recMap : Lake.NameMap Lake.Name