Bilel Ghorbel (Jul 18 2021 at 10:39): Bilel Ghorbel (Jul 18 2021 at 10:39):I am looking for the proper way to define a function that converts maps to lists.
My aim that the defined function is a right inverse of map_of for finite domain maps
Lukas Stevens (Jul 18 2021 at 11:46):If you use Mapping.thy from HOL-Library, then this is in the development version of Isabelle under Mapping.ordered_entries.
Bilel Ghorbel (Jul 18 2021 at 14:36):(deleted)
Bilel Ghorbel (Jul 18 2021 at 14:41):Does that means that I cannot find it or use it ? Because I don't seem to find it in the Mapping.thy file
Alexander Taepper (Jul 18 2021 at 14:46):You can take a look here https://isabelle-dev.sketis.net/source/isabelle/repository/default/ or specifically here https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/HOL/Library/Mapping.thy
Last updated: Apr 19 2024 at 12:27 UTC