Hi, what is the way of checking if an instance exists? E.g. checking if
wellorder exists for
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_classesand check what it says in the section for
thank you :)
Last updated: Aug 15 2022 at 02:13 UTC