Stream: Beginner Questions

Topic: Find instances


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Manuel Eberl (Jul 16 2021 at 19:24):

That doesn't work for more complex types though.

view this post on Zulip Manuel Eberl (Jul 16 2021 at 19:25):

You can also do print_classesand check what it says in the section for wellorder.

view this post on Zulip Robert Soeldner (Jul 16 2021 at 20:09):

thank you :)


Last updated: Dec 07 2024 at 16:22 UTC