Regarding open ... in

Stream: lean4

[Ioannis Konstantoulas]

I would like to open Nat in a theorem I am writing, but it seems like open ... in does not work as I expected. As a mwe, I want to remove the Nat prefix in the following:

theorem exampl : 0 < 1 :=
  Nat.zero_lt_of_ne_zero Nat.one_ne_zero

If I preface with open Nat in, I get

open Nat in
theorem exampl : 0 < 1 :=
  zero_lt_of_ne_zero one_ne_zero

unknown identifier 'one_ne_zero'

The first identifier is understood correctly as Nat. zero_lt_of_ne_zero, but the second one is not. Why is this, and what is the right way to open namespaces in restricted contexts?

[Ruben Van de Velde]

I suspect one_ne_zero is protected

[Ioannis Konstantoulas]

Ruben Van de Velde said:

I suspect one_ne_zero is protected

Ooh, thanks Ruben! I had forgotten about this possibility; I am sure that is why.

[Eric Wieser]

This works:

open Nat in
open Nat (one_ne_zero) in
theorem exampl : 0 < 1 :=
  zero_lt_of_ne_zero one_ne_zero

[Ioannis Konstantoulas]

Thanks for letting me know about this functionality!