Good morning, I would like to make a series of functions all depend on one datatype/type parameter. I figured maybe locales could help me as follows:
theory Scratch imports Main begin locale Foo = fixes proxy_to_get_type_var :: 'element_type begin datatype Inner = Inner 'element_type end end
Note that I don't plan on using
proxy_to_get_type_var; I figured I needed a way to indicate to the locale that I want at least one type parameter, and this seems to be the only way of doing it. In a way I'm trying to declare a type parameter.
Unfortunately Isabelle gives an error saying, at declaration of Inner, there is a free type variable on the right hand side. Instead, I would like it to use the
'element_type type parameter from the locale. I want this because then the subsequent datatypes don't need an extra type parameter, and this makes all function types a bit shorter.
I could add this type parameter everywhere to avoid using a locale. But I feel like it would be more readable like this. Am I doing something wrong or is there maybe some different construct I can use to emulate this?
Unfortunately, Isabelle/HOL does not have dependent types. This means that the type parameters can't depend on the local context (the locale in this case).
Last updated: Dec 07 2023 at 20:16 UTC