## Stream: new members

### Topic: locally disabling instances

#### 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.

#### Johan Commelin (Apr 02 2019 at 06:07):

I would also like to be able to do this.

#### 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

#### Scott Morrison (Apr 02 2019 at 07:22):

we need priority to take a with_bot nat

#### 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

#### 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.

#### 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