#227 (closed) shows that this is not obvious, and this is entirely fair.
However, this seems surprisingly inconsistent. The more consistent thing would be to use a GenNode
for each constructor, including non-recursive ones; then one also does not have to ever duplicate types in the big sum that is T
and one can always use the number in the node to indicate the constructor. Should we recommend that instead? If so, we should probably adjust the users, at least in the core std++ and Iris repos, to follow that pattern. We might even want to use a different definition then:
Inductive gen_tree (T : Type) : Type :=
| GenNode : nat → list T → list (gen_tree T) → gen_tree T.
The list of T
can be used to store arbitrary data of other types, and then the list of children is used for recursion only.