locally disabling instances

Stream: new members

[Scott Morrison]

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]

I would also like to be able to do this.

[Patrick Massot]

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]

we need priority to take a with_bot nat

[Simon Hudon]

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

[Scott Morrison]

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]

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