import init while hiding

Stream: new members

[John Hui]

I'm currently trying to clean up a translation of the Basics chapter of Logical Foundations, which redefines bool. My first draft had my own mybool sort of thing, because Lean does not seem to allow any kind of redeclaration/shadowing, but I was wondering if I could hide the standard library's definition?

I know sticking prelude at the top will hide imports, but it also hides the match tactic, which is kind of important:

prelude
inductive yo | foo | bar export yo
example (y: yo): yo :=
match y with -- nested exception message: cases tactic failed, it is not applicable to the given hypothesis
| foo := foo
| bar := bar
end

But then when I import init.meta, it seems to drag bool in all over again:

prelude
import init.meta
#check bool -- works...

[Mario Carneiro]

The match tactic is not required

[Mario Carneiro]

you can use yo.rec_on instead

[Mario Carneiro]

But if you go full prelude like this, you will not have the tactic framework so you can't use definitions by pattern matching

[Mario Carneiro]

But the usual recommendation is to either use mybool, or put everything in a namespace hidden

[Mario Carneiro]

Unfortunately it appears export does not respect namespaces so you have to fully qualify it, but otherwise this is just as good as the real thing

namespace hidden

inductive bool | tt | ff
export hidden.bool

example (y : bool) : bool :=
match y with
| tt := tt
| ff := ff
end

end hidden

[John Hui]

Thanks Mario! it looks like another downside with the namespace approach is that it does't appear to play well with notations:

namespace hidden
inductive bool | tt | ff
export hidden.bool
def orb /- ... -/
notation x `||` y := (orb x y)
example:  tt || ff -- ambiguous overload, possible interpretations

I'll probably use a mybool kind of approach

[Mario Carneiro]

use a local notation. Overloaded notation never works well, even in the standard library

[John Hui]

that worked, thanks!

[Kevin Buzzard]

Thanks for asking. I've seen this come up before in teaching situations. @Egbert Rijke did you know all these tips when you did your mylist student tutorial? Maybe they should be recorded somewhere? What does export do? I've never heard of it. I just move into the namespace and hope.

[Egbert Rijke]

I didn't know about the local notation. Thanks for tagging me!

[Mario Carneiro]

@Kevin Buzzard export is the global version of open

[Mario Carneiro]

for instance, in the core library there is export bool (tt ff) so that you can refer to tt anywhere without opening bool

[Kevin Buzzard]

Oh wow, I did not know that was a thing

[Mario Carneiro]

as with most global things, it should be used sparingly or in places where you don't care about the consequences