Zulip Chat Archive

Stream: lean4

Topic: Possible bug?


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jan 08 2021 at 19:34):

Thanks!

view this post on Zulip Jason KY. (Jan 08 2021 at 19:34):

Ah, I see! Thanks

view this post on Zulip Kenny Lau (Jan 08 2021 at 19:34):

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

view this post on Zulip Bryan Gin-ge Chen (Jan 08 2021 at 19:35):

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

view this post on Zulip Kenny Lau (Jan 08 2021 at 19:35):

oh it works for lower case Latin and Greek letters

view this post on Zulip Kenny Lau (Jan 08 2021 at 19:35):

that's nice

view this post on Zulip Kenny Lau (Jan 08 2021 at 19:36):

thanks


Last updated: May 07 2021 at 13:21 UTC