On 04/08/2022 17:49, Peter Lammich wrote:
In the AFP we have four separate copies of the definitionThe naming of the lemmas suggests that this function should be named lists, not list.definition list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set" where "list n A = {xs. size xs = n \<and> set xs \<subseteq> A}"
The motivation for "list" what is that in should mimic the name of the type constructor "list". On the level of types of rules omitted, e.g. nat not nats.
However I think these days I would also use the plural of the term level. Tobias
-- PeterInterestingly, the exact same concept is coded in three different ways in the four definitions. We also have a number of theorems in the repository referring to this concept:finite_lists_length_eq set_n_lists card_lists_length_eq lists_length_Suc_eqAnd we have three copies of Listn.thy in MicroJava and JinjaThreads. Could maybe some fragment of this, if not the whole thing, be moved into Library?Definitely, go ahead! (I obviously prefer the def you quoted above) TobiasLarry _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
