Stream: new members
Topic: Bug with letter H?
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.
Kenny Lau (Nov 04 2019 at 07:23):
∀ e ∈ S is sugar for
∀ e, ∀ H : e ∈ S
Kevin Buzzard (Nov 04 2019 at 07:44):
Kenny Lau (Nov 04 2019 at 07:44):
I just read the error message
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