List of lists

Stream: new members

[Edwin Agnew]

To better understand recursive types, I'm trying to create a type which is either 0 or a list of that type, e.g. [ [], 0, [0, []] ].
I tried defining this as
inductive plist : Type | zero : plist | li : (list plist) → plist
but that can't be right because it says unknown identifier when I try to use rec_on. What's gone wrong? Is there a better way to do this?

[Eric Wieser]

Sometimes rec_on isn't generated

[Eric Wieser]

plist.rec should still exist, which is the same thing with the arguments in a different order