prelude?

Stream: new members

[Thorsten Altenkirch]

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]

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]

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.

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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

[Yakov Pechersky]

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

[Kevin Buzzard]

You can probably use local notation for yours?

[Thorsten Altenkirch]

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]

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]

| is already used in set notation but hopefully there won't be a problem.