Zulip Chat Archive
Stream: lean4
Topic: Quotient.ind
Yuyang Zhao (Feb 19 2023 at 17:02):
Why docs4#Quotient.ind accepts a Quot Setoid.r, not Quotient s? This makes it unable to use the dot notation.
Eric Wieser (Feb 19 2023 at 17:08):
That looks like a bug to me. docs#quotient.ind is correct I think
Eric Wieser (Feb 19 2023 at 17:09):
Is this interfering with porting a file? If so, it _might_ be appropriate to create a Lean4 PR / issue, and reference it from the porting PR
Eric Wieser (Feb 19 2023 at 17:09):
(although I know that Lean4 is having trouble with the volume of contributions at the moment)
Bulhwi Cha (Feb 19 2023 at 17:34):
See my PR: lean4#2111 (New PR: lean4#2114).
Eric Wieser (Feb 19 2023 at 17:42):
That PR is a bit misleadingly titled; it's not just a doc change
Bulhwi Cha (Feb 19 2023 at 17:54):
I'll split the commit into two and make another PR after I wake up from sleep.
Bulhwi Cha (Feb 20 2023 at 01:07):
I've closed the previous PR and opened a new one. See lean4#2114.
Last updated: Dec 20 2023 at 11:08 UTC