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
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.
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.
Thanks, you helped me :). I'll choose the latter.
Yay the error is gone. Time to party.
Last updated: Dec 07 2023 at 20:16 UTC