Bob Rubbens (May 06 2023 at 09:45): Bob Rubbens (May 06 2023 at 09:45):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?
Lukas Stevens (May 08 2023 at 08:48):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: Apr 28 2024 at 16:17 UTC