I introduce variables with fix A :: "'a set"
, which I later use and need 'a
to have a specific typeclass. Is there a way to fix variables with the additional restriction that they are in a typeclass?
fix A :: "`a :: myclass set"
Now I get the following though:
Sort constraint linorder inconsistent with default type for type variable "'a"
Then you already have a type 'a
in your context that doesn't have that type class.
So you probably have to annotate it with that type class even earlier.
Come to think of it, I don't think I can think of any common situation where it would be required to add a type class annotation to a fix
command.
If you don't understand what you need to do, you should perhaps post some more context so that we can see what it is that you are attempting to do.
Yeah I have a (in linorder)
on my lemma, and yet it complains that 'a
isn't of sort linorder.
My lemma:
lemma (in linorder): "myprop myfunc"
unfolding myprop_def
proof (safe)
fix A :: "'a set"
have "..." using other_lemma[of A] (* <-- error here that A is not of sort linorder*)
qed
I hope that's enough code.
Ah, yes, this is an oddity of the way type classes work in Isabelle. When you are in the linorder
context, you do not actually have the sort linorder
on the type variable 'a
and there is no way to get it.
Ideally, you should prove your other_lemma
also in a linorder
context (i.e. with in linorder
) so that you can use it here.
If that is not possible for some reason, you will have to prove everything that builds on it also outside the linorder
context, with an explicit linorder
sort annotation.
Explicit sort annotation such as 'a :: linorder
? Just making sure, since I'm not a pro on sorts.
Yes.
Thanks, you helped me :). I'll choose the latter.
Yay the error is gone. Time to party.
Last updated: Dec 07 2024 at 16:22 UTC