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
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
Last updated: May 10 2021 at 18:22 UTC