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