Stream: new members
Thorsten Altenkirch (Sep 13 2020 at 15:49):
How do I find what exactly is preloaded in lean? I mean staff like natural numbers booleans are already defined. Where do I find all the definitions?
Thorsten Altenkirch (Sep 13 2020 at 16:01):
Ok, I found it. However, I would like to use some library functions as examples and I would prefer to use the same names not to confuse the students. How can I avoid loading at least part of the core? So for example I want to define
def bnot : bool → bool | tt := ff | ff := tt
but obviously I get an error. :-(
Reid Barton (Sep 13 2020 at 16:10):
If you write
prelude at the top of your file then nothing will be implicitly imported.
Whether this is a good approach is a separate question... you will also be missing (for example) all tactics, and importing those will possibly import other stuff you don't want. So another option is to put all your custom stuff in a
Kevin Buzzard (Sep 13 2020 at 16:30):
I use namespaces when teaching: if you
namespace foo and then define
bnot then, within the
foo namespace, Lean will (hopefully) prefer your
bnot to the builtin one.
Thorsten Altenkirch (Sep 13 2020 at 16:40):
Ok but now I notice that namespaces don't allow me to redefine notations. :-(
Sorry but coming from agda the lean syntax is positively Stone Age.
Kevin Buzzard (Sep 13 2020 at 16:41):
This is interesting to hear -- I've had no experience with other provers at all so I don't know what I'm missing out on. There are all sorts of tricks you can do with notation, so I wouldn't give up hope yet. What exactly are you trying to do? NB notation in Lean 4 will be better, but there's still no release.
Thorsten Altenkirch (Sep 13 2020 at 16:43):
In Agda infix (or even mixfix) identifiers are written like this _&&_ and the arguments go where the underlines are. So I can redefine it like any other function. Only disadvantages you have to use spaces to separate tokens (but one gets used to this very quickly).
Thorsten Altenkirch (Sep 13 2020 at 16:45):
Basically I tried to redefine && and || because I think the prelude definitions are brain damaged. Or to be more polite: my examples don't work because I have uneccessarily to match on the 2nd argument. My way out is now to use & and | instead. Maybe this is actually better then redefining the ones which are there.
Kevin Buzzard (Sep 13 2020 at 16:53):
The equation compiler does not always define things the way you expect them to be defined, when matching on more than one thing:
#print prefix <what you just defined> is always worth inspecting.
Yakov Pechersky (Sep 13 2020 at 16:55):
What's the error you're seeing about notation?
Yakov Pechersky (Sep 13 2020 at 16:56):
Do you mean that && is fixed to be the notation for the root band?
Kevin Buzzard (Sep 13 2020 at 16:56):
You can probably use local notation for yours?
Thorsten Altenkirch (Sep 13 2020 at 17:24):
61:53: ambiguous overload, possible interpretations notb x && notb y notb x && notb y
actually now I have decided to use & and | instead since I am defining the operations in a different way anyway.
Yakov Pechersky (Sep 13 2020 at 17:36):
I think defining notation locally (using keyword local) can override any previous notation, but I'm not sure. You could possibly also change the has_and instance to point to your definition instead.
Kevin Buzzard (Sep 13 2020 at 17:37):
| is already used in set notation but hopefully there won't be a problem.
Last updated: May 14 2021 at 21:11 UTC