Zulip Chat Archive

Stream: triage

Topic: PR #4615: feat(tactic/converter): Add an exact tactic, to...


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

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

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

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

view this post on Zulip Eric Wieser (Feb 01 2021 at 14:26):

Two days in a row!

view this post on Zulip Rob Lewis (Feb 01 2021 at 14:48):

Eric Wieser said:

Two days in a row!

Ugh, it's not supposed to do that

view this post on Zulip Rob Lewis (Feb 01 2021 at 15:18):

Fixed, I hope. https://github.com/leanprover-community/azure-scripts/commit/f708f614b8da944fd2dd57184ee4c51c3fe4384b

view this post on Zulip 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: May 18 2021 at 23:14 UTC