From b38cea43911968382246acbf2dadfc3aaeae9cfc Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Mon, 17 Feb 2025 08:29:24 +0100 Subject: [PATCH 1/2] gen_tree: add comment explaining intended usage --- stdpp/countable.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/stdpp/countable.v b/stdpp/countable.v index 5677e2d6..ebcd0f93 100644 --- a/stdpp/countable.v +++ b/stdpp/countable.v @@ -313,6 +313,15 @@ Qed. (** ** Generic trees *) Local Close Scope positive. +(** This type can help you construct a [Countable] instance for an arbitrary +(even recursive) inductive datatype. The idea is tht you make [T] something like +`T1 + T2 + ...`, covering all the data types that can be contained inside your +type. +- Each non-recursive constructor to a [GenLeaf]. Different constructors must use + different variants of [T] to ensure they remain distinguishable! +- Each recursive constructor to a [GenNode] where the [nat] is a (typically + small) constant representing the constructor itself, and then all the data in + the constructor (recursive or otherwise) is put into child nodes. *) Inductive gen_tree (T : Type) : Type := | GenLeaf : T → gen_tree T | GenNode : nat → list (gen_tree T) → gen_tree T. -- GitLab From 3b269ef3b688ca88a2360969b0e936cbe50f2bcb Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 18 Feb 2025 07:29:37 +0000 Subject: [PATCH 2/2] improve comment --- stdpp/countable.v | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/stdpp/countable.v b/stdpp/countable.v index ebcd0f93..73993ceb 100644 --- a/stdpp/countable.v +++ b/stdpp/countable.v @@ -315,13 +315,16 @@ Local Close Scope positive. (** This type can help you construct a [Countable] instance for an arbitrary (even recursive) inductive datatype. The idea is tht you make [T] something like -`T1 + T2 + ...`, covering all the data types that can be contained inside your +[T1 + T2 + ...], covering all the data types that can be contained inside your type. - Each non-recursive constructor to a [GenLeaf]. Different constructors must use different variants of [T] to ensure they remain distinguishable! - Each recursive constructor to a [GenNode] where the [nat] is a (typically small) constant representing the constructor itself, and then all the data in - the constructor (recursive or otherwise) is put into child nodes. *) + the constructor (recursive or otherwise) is put into child nodes. + +This data type is the same as `GenTree.tree` in mathcomp, see +https://github.com/math-comp/math-comp/blob/master/ssreflect/choice.v *) Inductive gen_tree (T : Type) : Type := | GenLeaf : T → gen_tree T | GenNode : nat → list (gen_tree T) → gen_tree T. -- GitLab