Hanna Lachnitt (Sep 01 2023 at 21:38): Hanna Lachnitt (Sep 01 2023 at 21:38):Hi everyone,
sorry if this has been asked already. I have written a definition with an additional type variable. I want to include it explicitly so I can instantiate it later. This is a minimal example I made
definition test :: "'a::len word ⇒ 'b::len word ⇒ bool" where
"test x y = (Word.word_cat x y = 0)"
Now of course I get a warning about 'c . I remember there was a way to avoid this warning by explicitly telling Isabelle: "Yeah I know about 'c and it is not a mistake" but forgot how exactly it works.
Looking at the manual:
I first thought it is part of the for_fixes:
but if I add for "_::'c" I get a legacy feature warning and a bad name error. How do I do this without introducing an extra variable of that type explicitely?
Lukas Stevens (Sep 01 2023 at 22:01):Normally you can do something like this
definition test :: "''c itself => a::len word ⇒ 'b::len word ⇒ bool" where
"test TYPE('c) x y = (Word.word_cat x y = 0)"
I don't know how much sense it makes in this case to instantiate the type since the type indicates the length of the resulting word, i.e. you need to pass a type that has the right cardinality.
Lukas Stevens (Sep 01 2023 at 22:02):(This example does not allow you to specify 'c it just shows how you can pass a type in principle)
Lukas Stevens (Sep 01 2023 at 22:10):Got it:
definition test :: "'c::len itself ⇒ 'a::len word ⇒ 'b::len word ⇒ bool" where
"test TYPE('c) x y ⟷ ((Word.word_cat x y) :: 'c word) = 0"
Thanks a lot, that is exactly what I wanted!
Last updated: Apr 28 2024 at 01:11 UTC