Email Gateway (Aug 19 2022 at 12:01): Email Gateway (Aug 19 2022 at 12:01):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
for a project of mine, I had to define a "group" function on lists, and
I think this might be of enough general interest to be added to the
library; I am not entirely sure whom I am supposed to contact in these
matters, so I thought it would be best to just post it on the mailing list.
The function does something similar to Haskell's group function, but not
quite the same. The function "merges" all adjacent equal elements of a
list, e.g. it turns [1,2,2,3,3,3,2,2,1] into [1,2,3,2,1].
(This function has type 'a list ⇒ 'a list, whereas the Haskell function
"group" has type 'a list ⇒ 'a list list, it turns [1,2,2] not into
[1,2], like my function, but into [[1],[2,2]])
I attached an Isabelle theory with the function definition and proofs
for some basic properties.
Cheers,
Manuel
List_Group.thy
Email Gateway (Aug 19 2022 at 12:01):From: Tobias Nipkow <nipkow@in.tum.de>
Thanks, I'll import it into List as merge_eq.
Tobias
Last updated: Apr 25 2024 at 20:15 UTC