Zulip Chat Archive

Stream: general

Topic: structure projection + implicit arguments


view this post on Zulip Kenny Lau (Oct 28 2020 at 08:44):

axiom foo :  (m : ) {n : }, m = n

#check foo 0 -- foo 0 : 0 = ?M_1

structure bar : Prop :=
(baz :  {m : }, m = 0)

variables (h : bar)

#check h.baz -- h.baz : ∀ {m : ℕ}, m = 0
#check bar.baz h -- h.baz : ?M_1 = 0

view this post on Zulip Kenny Lau (Oct 28 2020 at 08:44):

should h.baz be ?M_1 = 0 also?

view this post on Zulip Kenny Lau (Oct 28 2020 at 09:43):

@Mario Carneiro

view this post on Zulip Mario Carneiro (Oct 28 2020 at 09:45):

Yeah, this is the same bug I mentioned to Yasmine yesterday

view this post on Zulip Mario Carneiro (Oct 28 2020 at 09:46):

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Projecting.20Class.20Members/near/214645426

view this post on Zulip Mario Carneiro (Oct 28 2020 at 09:48):

Is there a lean issue for this?

view this post on Zulip Mario Carneiro (Oct 28 2020 at 10:01):

lean#492

view this post on Zulip Kenny Lau (Oct 28 2020 at 10:02):

thanks


Last updated: May 14 2021 at 06:16 UTC