structure projection + implicit arguments

Stream: general

[Kenny Lau]

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

[Kenny Lau]

should h.baz be ?M_1 = 0 also?

[Kenny Lau]

@Mario Carneiro

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

Is there a lean issue for this?

[Mario Carneiro]

lean#492

[Kenny Lau]

thanks