undefine or hide core library?

Stream: new members

[Peter B]

I recognize this is not a typical use case, but: is there some mechanism to undefine or hide everything defined in core.lean? (I'm still just in the "playing with the language" state so I'm asking more from curiosity than anything.)

[Alex J. Best]

You can use the command prelude to exclude everything in init

[Peter B]

The answer might be "Don't do that, then!" but when I try to view this in either emacs or VSCode with the lean 4 (stable) toolchain

prelude

inductive bool : Type
| true : bool
| false : bool

def negb (b : bool) : bool :=
match b with
  | bool.true => bool.false
  | bool.false => bool.true

open boolean
#check negb true

I get unknown constant 'sorryAx' [2 times] at or around the match b line.

If I remove "prelude" and rename bool to something unique/not overloaded, it compiles fine.

[Peter B]

If I then import (for example) Lean.Util.Sorry, then bool is declared (presumably because that file implicitly or explicitly depends on the stuff in Prelude)

[Julian Berman]

Are you perhaps trying to do this?

namespace Peter

inductive bool : Type
| true : bool
| false : bool

def negb (b : bool) : bool :=
match b with
  | bool.true => bool.false
  | bool.false => bool.true

open bool
#check negb true

end Peter

[Julian Berman]

Using prelude strictly speaking satisfies what you were originally asking for (by undefining lots of stuff) but as you're finding it then requires you to define a bunch of stuff. I'm not sure whether it's even specified what stuff needs to go in a custom prelude to get various functionality to work again, probably it is -- but if you instead really mean to define your own versions of things, you might instead yeah use a namespace like ^ where now technically speaking you're defining Peter.bool but are free to do so without it clashing with the root bool.

[Peter B]

Possibly? I don't think that works either, though, let me re-try it.

[Peter B]

Grrr that sure does work!

[Peter B]

Thank you!