Behavior of unknown identifier error

Stream: lean4

[Yasu Watanabe]

The following code produces one unknown identifier error.

namespace A
inductive A1 where
| a1 : A1
end A

inductive A1 where
| a1 : A1

structure Example where
  ok : A1 -- This should be OK
  not_error : A2 -- This does not produce error
  ok' : A.A1  -- A.A1 is defined.
  ok'' : A.A2 -- unknown identifier 'A.A2'

This behavior is a bit annoying when I typo. If this is expected, I'd like to know to disable this feature.

Note that as far as i tried, nightly-2022-02-08 produces two errors.

[Horatiu Cheval]

You can disable the feature with set_option autoImplicit false

[Horatiu Cheval]

namespace A
inductive A1 where
| a1 : A1
end A

inductive A1 where
| a1 : A1

set_option autoImplicit false

structure Example where
  ok : A1 -- This should be OK
  not_error : A2 -- This does not produce error
/-
  unknown identifier 'A2'
-/

[Horatiu Cheval]

On older versions, I think the option used to be called autoBoundImplicitLocal btw. I'm not sure if your 2022-02-08 nightly is before or after the change

[Yasu Watanabe]

Horatiu Cheval said:

You can disable the feature with set_option autoImplicit false

Oh, thanks. I've found several typos with this option.