Zulip Chat Archive

Stream: triage

Topic: PR #4718: feat(tactic/explode): display exploded proofs a...


view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Nov 08 2020 at 19:13):

This one is waiting on the author for doc strings.

view this post on Zulip Mario Carneiro (Nov 08 2020 at 19:25):

This is LGTM from me, I don't have anything in particular to add

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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: May 09 2021 at 16:20 UTC