Christian Pardillo Laursen (Jul 13 2024 at 12:49): Christian Pardillo Laursen (Jul 13 2024 at 12:49):Hi. I'd like to define a type of functions similar to the haskell type
forall s. (s -> a) -> s -> a
Effectively, I'd like to restrict functions of this type to only be able to use the "s" value they have received, and not produce any of their own. Is there any way to do this in Isabelle? Not necessarily at the type level, as I understand the types of Isabelle are a bit weaker than System F.
Last updated: Dec 21 2024 at 12:33 UTC