Namespaces and rfl

Stream: new members

[Trevor Hyde]

I have a question about this example from Theorem Proving in Lean 4:

namespace Hidden
inductive Nat where
 | zero : Nat
 | succ : Nat → Nat
 deriving Repr
namespace Nat

def add (m n : Nat) : Nat :=
  match n with
  | Nat.zero   => m
  | Nat.succ n => Nat.succ (add m n)

instance : Add Nat where
  add := add

theorem add_zero (m : Nat) : m + zero = m := rfl
theorem add_succ (m n : Nat) : m + succ n = succ (m + n) := rfl

end Nat
end Hidden

If I change the namespace from Nat to Foo, the rfl tactic does not work to prove these theorems. Why does the namespace have to match the type Nat? What is the general rule here?

[Ruben Van de Velde]

If you add

set_option autoImplicit false

you get better error messages:

unknown identifier 'zero'
unknown identifier 'succ'

[Ruben Van de Velde]

If you're in a namespace Foo, the variants of an inductive type Foo are automatically in scope