Zulip Chat Archive
Stream: triage
Topic: PR #10348: Add whilecc.lean
Random Issue Bot (Feb 01 2022 at 14:16):
Today I chose PR 10348 for discussion!
Add whilecc.lean
Created by @Leo Okawa Ericson (@Zetagon) on 2021-11-16
Labels: please-adopt
Is this PR still relevant? Any recent updates? Anyone making progress?
Arthur Paulino (Feb 01 2022 at 14:20):
This PR adds 1,250 lines :open_mouth:
Ruben Van de Velde (Feb 01 2022 at 14:21):
Might be why it hasn't landed yet :)
Patrick Massot (Feb 01 2022 at 14:23):
The description also contains: "I know that it doesn't fully comply with the mathlib style and some definitions are redundant with definitions in mathlib proper. "...
Arthur Paulino (Feb 01 2022 at 14:24):
Yeah, it's hard to approach this one
Random Issue Bot (Apr 07 2022 at 14:13):
Today I chose PR 10348 for discussion!
Add whilecc.lean
Created by @Leo Okawa Ericson (@Zetagon) on 2021-11-16
Labels: please-adopt
Is this PR still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC