On 04/08/2022 15:50, Lawrence Paulson wrote:
In the AFP we have four separate copies of the definition definition list :: "nat \<Rightarrow> 'a set \<Rightarrow> 'a list set" where "list n A = {xs. size xs = n \<and> set xs \<subseteq> A}"Interestingly, 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) Tobias
Larry _______________________________________________ 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
