Robert Soeldner (Jul 16 2021 at 18:28): Robert Soeldner (Jul 16 2021 at 18:28):Hi, what is the way of checking if an instance exists? E.g. checking if wellorder exists for nat?
Manuel Eberl (Jul 16 2021 at 19:22):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.
Mathias Fleury (Jul 16 2021 at 19:23):I usually try to instantiate it again with sorry and see if it produces an error or not
Manuel Eberl (Jul 16 2021 at 19:24):That doesn't work for more complex types though.
Manuel Eberl (Jul 16 2021 at 19:25):You can also do print_classesand check what it says in the section for wellorder.
Robert Soeldner (Jul 16 2021 at 20:09):thank you :)
Last updated: Apr 24 2024 at 12:33 UTC