autoImplicit confusion?

Stream: mathlib4

[James Gallicchio]

Does this compile due to auto implicit binding or for another reason?

inductive Foo
| bar (x)

Doing set_option autoImplicit false doesn't cause it to fail

[James Gallicchio]

And since I assume it's a different lean4 feature, is there some way to disable it?

I don't really mind the behavior here, but another student was asking

[Wojciech Nawrocki]

This looks like a bug in autoImplicit.

set_option autoImplicit false in
inductive Foo
| bar (x) : Foo

/- @Foo.bar : {x : Sort u_1} → x → Foo -/
#check @Foo.bar

set_option autoImplicit false in
inductive Foo'
/- unknown identifier 'x' -/
| bar : x → Foo'