gen_tree: add comment explaining intended usage
#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.
Merge request reports
Activity
added 1 commit
- b38cea43 - gen_tree: add comment explaining intended usage
The comment looks good to me.
With regarding to changing the definition, I do not have a very strong opinion. Just to say, the original definition is the same as the one in math-comp, https://github.com/math-comp/math-comp/blob/master/ssreflect/choice.v#L171 We should actually credit that in the comments.
enabled an automatic merge when all merge checks for 3b269ef3 pass
mentioned in issue #227 (closed)
mentioned in commit d99d3967
