Remove core lib definition from local context

Stream: new members

[Michael Palm]

Hi,

is it possible to remove a definition from the core lib from the local context?

To be precise, I find the def not (a : Prop) := a → false definition unpleasant.
I would prefer to define constant not : Prop → Prop and define an axiom
axiom not.intro {A : Prop} : (A → false) → ¬A

Is that possible? Are there obvious drawbacks? I do not require mathlib or anything else beyond the core lib... (at least I think so :-D)

Kind regards,
Michael

[Ruben Van de Velde]

I suspect getting used to it will be the more productive approach

[Andrew Yang]

You can start your file with a line

prelude

which will hide the definitions from the core lib.

[Andrew Yang]

Regarding the not, you will also need an not.elim {A B : Prop} : ¬A → A → B.

[Michael Palm]

I know prelude. But it also prevents all other import of the Init scripts. This makes tactics unusable.

[Yakov Pechersky]

Let's say you removed a core def. How would you like all of the parts of core that used the def to now work?

[Yaël Dillies]

Andrew Yang said:

Regarding the not, you will also need an not.elim {A B : Prop} : ¬A → A → B.

Actually, Michael would rather need not.elim {A : Prop} {B : Sort*} : ¬A → A → B.

[Eric Wieser]

Would the following work for you, Michael?

structure my_not (A : Prop) :=
intro :: (elim' : A →false)

rather than using axioms?

[Kevin Buzzard]

Instead of removing not, why not just define not'? (e.g. the way Eric defined it)