Zulip Chat Archive

Stream: new members

Topic: Bug with letter H?


view this post on Zulip Li Yao'an (Nov 04 2019 at 07:21):

Consider the following code:

structure X :=
mk :: (adj : Prop)

constant S: set ℕ

def th1 (K : X) :=
        ∀ e ∈ S, K.adj

def th2 (H : X) :=
        ∀ e ∈ S, H.adj

def th3 (Q : X) :=
        ∀ e ∈ S, Q.adj

Is there a reason why Lean (online editor/VS) only throws an error for th2 when the letter H is used? This looks like a bug to me.

view this post on Zulip Kenny Lau (Nov 04 2019 at 07:23):

∀ e ∈ S is sugar for ∀ e, ∀ H : e ∈ S

view this post on Zulip Kevin Buzzard (Nov 04 2019 at 07:44):

Good catch

view this post on Zulip Kenny Lau (Nov 04 2019 at 07:44):

I just read the error message

view this post on Zulip Li Yao'an (Nov 04 2019 at 09:51):

Thanks for the reply. It makes sense now!


Last updated: May 14 2021 at 00:42 UTC