Hi, what is the way of checking if an instance exists? E.g. checking if wellorder
exists for nat
?
I don't know of a proper way to do this, but what I often do is to define a dummy function like
definition f :: "'a :: wellorder ⇒ 'a" where
"f x = x"
and then do
term "f (x :: nat)"
and see if that gives me an error or not.
I usually try to instantiate it again with sorry and see if it produces an error or not
That doesn't work for more complex types though.
You can also do print_classes
and check what it says in the section for wellorder
.
thank you :)
Last updated: Dec 07 2024 at 16:22 UTC