Zulip Chat Archive

Stream: new members

Topic: prelude?


view this post on Zulip 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?

view this post on Zulip 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. :-(

view this post on Zulip 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 namespace.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Sep 13 2020 at 16:55):

What's the error you're seeing about notation?

view this post on Zulip Yakov Pechersky (Sep 13 2020 at 16:56):

Do you mean that && is fixed to be the notation for the root band?

view this post on Zulip Kevin Buzzard (Sep 13 2020 at 16:56):

You can probably use local notation for yours?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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