## Stream: lean4

### Topic: Possible bug?

#### Jason KY. (Jan 08 2021 at 19:30):

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 (Jan 08 2021 at 19:32):

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


Thanks!

#### Jason KY. (Jan 08 2021 at 19:34):

Ah, I see! Thanks

#### Kenny Lau (Jan 08 2021 at 19:34):

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

#### Kenny Lau (Jan 08 2021 at 19:35):

oh it works for lower case Latin and Greek letters

that's nice

#### Kenny Lau (Jan 08 2021 at 19:36):

thanks

Last updated: May 07 2021 at 13:21 UTC