Email Gateway (Aug 19 2022 at 16:17): Email Gateway (Aug 19 2022 at 16:17):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
I just updated
https://sourceforge.net/projects/holcf-prelude/
(something similar to the Haskell Prelude based on HOLCF) to Isabelle2014.
As already reported earlier
https://sourceforge.net/projects/holcf-prelude/
I had some trouble adapting fixrecs involving case syntax.
This time it kind of worked. Only kind of, since it seems that it makes
a difference whether dummy variables ("_") are used in patterns of case
branches or not (without "_" everything seems to be fine).
Please find a small theory file attached that gives an example of what I
mean.
Any thoughts?
cheers
chris
Test.thy
Last updated: Apr 30 2024 at 04:19 UTC