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: Nov 11 2024 at 01:24 UTC