Zulip Chat Archive
Stream: triage
Topic: PR #4718: feat(tactic/explode): display exploded proofs a...
Random Issue Bot (Nov 08 2020 at 14:17):
Today I chose PR 4718 for discussion!
feat(tactic/explode): display exploded proofs as widgets
Created by @Minchao Wu (@minchaowu) on 2020-10-20
Labels: awaiting-author, meta
Is this PR still relevant? Any recent updates? Anyone making progress?
Bryan Gin-ge Chen (Nov 08 2020 at 19:13):
This one is waiting on the author for doc strings.
Mario Carneiro (Nov 08 2020 at 19:25):
This is LGTM from me, I don't have anything in particular to add
Random Issue Bot (Nov 20 2020 at 14:19):
Today I chose PR 4718 for discussion!
feat(tactic/explode): display exploded proofs as widgets
Created by @Minchao Wu (@minchaowu) on 2020-10-20
Labels: awaiting-author, meta, needs-documentation
Is this PR still relevant? Any recent updates? Anyone making progress?
Rob Lewis (Nov 20 2020 at 15:36):
@Minchao Wu this is waiting on documentation, I think. It looks really nice and I'd love to see it in the library!
Minchao Wu (Nov 21 2020 at 06:14):
@Rob Lewis thanks for the reminder, done! (The previous mentions in this thread didn't seem to have reached me.)
Last updated: Dec 20 2023 at 11:08 UTC