Zulip Chat Archive

Stream: new members

Topic: locally disabling instances


view this post on Zulip Scott Morrison (Apr 02 2019 at 04:07):

Can one entirely turn off an already imported instance, locally? You can override it by providing something with higher priority, and I was hoping that [priority 0] might remove it from the search, but that doesn't seem to happen.

view this post on Zulip Johan Commelin (Apr 02 2019 at 06:07):

I would also like to be able to do this.

view this post on Zulip Patrick Massot (Apr 02 2019 at 07:13):

priority 0 cannot be the answer, this is what we use for decidability to ensure it is used only after all actual instances. But we do want to use it

view this post on Zulip Scott Morrison (Apr 02 2019 at 07:22):

we need priority to take a with_bot nat

view this post on Zulip Simon Hudon (Apr 02 2019 at 12:12):

Why do you need to disable an instance? Maybe there's another way to approach the issue

view this post on Zulip Scott Morrison (Apr 02 2019 at 22:03):

I asked this mostly for the sake of teaching students about instances -- I had them building by hand some instances that already existed, and it was sometimes confusing whether library or hand-built instances were being used.

view this post on Zulip Simon Hudon (Apr 02 2019 at 22:06):

You could try using synonyms for the types you're building instances for. For instance, if you want the students to build an instance of monoid nat, write a definition def natural := nat and then an instance monoid natural


Last updated: May 10 2021 at 18:22 UTC