Possible bug?

Stream: lean4

[Jason KY.]

Hi, I'm using lean4.0.0-m1 and I've encountered the following

def bar (s t : α → Prop) := ∀ x, s x → t x

def foo : α → Prop := λ x => True

theorem hi.foo {s : α → Prop} : bar s foo := sorry

theorem hi.anothername {s : α → Prop} : bar s foo := sorry -- Error here

The error is

application type mismatch
  bar s foo
argument
  foo
has type
  bar ?m.110 foo
but is expected to have type
  α → Prop

It seems that the error only occurs whenever hi.foo has the same name as foo even though they are in different namespace, that is the error does not occur if I change hi.foo to hi.foo1.

[Leonardo de Moura]

No, this is not a bug.

theorem hi.anothername {s : α → Prop} : bar s foo := sorry

is expanded into

namespace hi
theorem anothername {s : α → Prop} : bar s foo := sorry -- So, `hi` here is `hi.foo`
end hi

[Kenny Lau]

Thanks!

[Jason KY.]

Ah, I see! Thanks

[Kenny Lau]

Also, how does it compile without us specifying what \a is?

[Bryan Gin-ge Chen]

@Kenny Lau https://leanprover.github.io/lean4/doc/autobound.html

[Kenny Lau]

oh it works for lower case Latin and Greek letters

[Kenny Lau]

that's nice

[Kenny Lau]

thanks