Zulip Chat Archive
Stream: triage
Topic: PR #4615: feat(tactic/converter): Add an exact tactic, to...
Random Issue Bot (Nov 19 2020 at 14:21):
Today I chose PR 4615 for discussion!
feat(tactic/converter): Add an exact tactic, to allow dropping back into tactic mode
Created by @Eric Wieser (@eric-wieser) on 2020-10-14
Labels: awaiting-author, meta
Is this PR still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Dec 19 2020 at 14:26):
Today I chose PR 4615 for discussion!
feat(tactic/converter): Add an exact tactic, to allow dropping back into tactic mode
Created by @Eric Wieser (@eric-wieser) on 2020-10-14
Labels: awaiting-author, meta
Is this PR still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jan 31 2021 at 14:23):
Today I chose PR 4615 for discussion!
feat(tactic/converter): Add an exact tactic, to allow dropping back into tactic mode
Created by @Eric Wieser (@eric-wieser) on 2020-10-14
Labels: awaiting-author, meta
Is this PR still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Feb 01 2021 at 14:24):
Today I chose PR 4615 for discussion!
feat(tactic/converter): Add an exact tactic, to allow dropping back into tactic mode
Created by @Eric Wieser (@eric-wieser) on 2020-10-14
Labels: awaiting-author, meta
Is this PR still relevant? Any recent updates? Anyone making progress?
Eric Wieser (Feb 01 2021 at 14:26):
Two days in a row!
Rob Lewis (Feb 01 2021 at 14:48):
Eric Wieser said:
Two days in a row!
Ugh, it's not supposed to do that
Rob Lewis (Feb 01 2021 at 15:18):
Fixed, I hope. https://github.com/leanprover-community/azure-scripts/commit/f708f614b8da944fd2dd57184ee4c51c3fe4384b
Random Issue Bot (Mar 11 2021 at 14:26):
Today I chose PR 4615 for discussion!
feat(tactic/converter): Add an exact tactic, to allow dropping back into tactic mode
Created by @Eric Wieser (@eric-wieser) on 2020-10-14
Labels: awaiting-author, meta
Is this PR still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC