Global definition shadowing a local one

Stream: new members

[Nikolai Morin]

Hi folks, I'm learning Lean with Advent of Code and quickly falling in love with the language and its documentation :) One thing tripped me up: when I write

def digits: List String := ["1", "2", "3", "4", "5", "6", "7", "8", "9"]

def process (s: String) : Nat :=
  digits.foldl (fun (n : Nat) (c : Char) => n*10 + (c.toNat - '0'.toNat)) 0
  where digits: List Char := s |> String.toList |> List.filter Char.isDigit |> firstAndLast

then the global digits shadows the "local variable" digits instead of the other way around. That was very unexpected, since usually programming languages prefer definition from inner scopes. Is there a good reason not to do it in the usual way?

[Patrick Massot]

@Sebastian Ullrich?

[Sebastian Ullrich]

Interesting, I don't think anyone has tried that before. It is certainly worth a bug report.

[Nikolai Morin]

Sebastian Ullrich said:

Interesting, I don't think anyone has tried that before. It is certainly worth a bug report.

Cool, I'll just open an issue on GitHub then?

[Eric Wieser]

This only happens when using dot notation it seems

[Eric Wieser]

def foo : Nat := 1

def bar : Nat :=
  foo.add 1
where
  foo := 10

def baz : Nat :=
  .add foo 1
where
  foo := 10

#eval bar -- 2
#eval baz -- 11

[Nikolai Morin]

Thanks Eric, probably best if I use your simplified example in the bug description. Edit: https://github.com/leanprover/lean4/issues/3079