Lean 4 not recognizing undefined variable

Stream: lean4

[Bolton Bailey]

I was having trouble with a particular variable that I was being told had a particular type I didn't think it should have. Interestingly, when I deleted the definition for this variable I didn't get any kind of undeclared identifier error. What is going on here?

import Std.Data.List.Basic

def foobar (p : Nat)  : Nat := sorry

structure abc :=
  (defg : (foobar bazqux = 1))

[Bolton Bailey]

I guess lean just assumes it's an implicit argument?

[Adrien Champion]

That is correct you can add the following after structure abc := ... to inspect what's going on:

#check abc.defg
-- abc.defg : abc → ∀ {bazqux : Nat}, foobar bazqux = 1

[Jireh Loreaux]

You can turn off the auto implicit feature with set_option autoImplicit false

[Gabriel Ebner]

Some other ways you can spot this:

• If you use vscode or emacs, then the bazqux will be highlighted differently if it's a local variable or a constant.
• You can hover over abc (instead of writing #check abc) to see the extra parameter.

[Adrien Champion]

Gabriel Ebner said:

Some other ways you can spot this:

• If you use vscode or emacs, then the bazqux will be highlighted differently if it's a local variable or a constant.
• You can hover over abc (instead of writing #check abc) to see the extra parameter.

"hover over defg", abc is just Type

def foobar (p : Nat)  : Nat := sorry

structure abc :=
  (defg : (foobar bazqux = 1))
#check abc
-- abc : Type
#check @abc.defg
-- abc.defg : abc → ∀ {bazqux : Nat}, foobar bazqux = 1

[Gabriel Ebner]

Should have tested it first.