Zulip Chat Archive
Stream: triage
Topic: issue #2724: have `solve_by_elim` call `intro1` before gi...
Random Issue Bot (Jan 21 2021 at 14:44):
Today I chose issue 2724 for discussion!
have solve_by_elim call intro1 before giving up
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: feature-request, help wanted, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jan 31 2021 at 14:23):
Today I chose issue 2724 for discussion!
have solve_by_elim call intro1 before giving up
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: feature-request, help wanted, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Oct 15 2021 at 14:18):
Today I chose issue 2724 for discussion!
have solve_by_elim call intro1 before giving up
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help wanted, meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Aug 26 2022 at 14:13):
Today I chose issue 2724 for discussion!
have solve_by_elim call intro1 before giving up
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help wanted, t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Nov 03 2022 at 14:22):
Today I chose issue 2724 for discussion!
have solve_by_elim call intro1 before giving up
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help wanted, t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jan 26 2023 at 14:08):
Today I chose issue 2724 for discussion!
have solve_by_elim call intro1 before giving up
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help wanted, t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Mar 14 2023 at 14:09):
Today I chose issue 2724 for discussion!
have solve_by_elim call intro1 before giving up
Created by @Scott Morrison (@semorrison) on 2020-05-18
Labels: help wanted, t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Scott Morrison (Mar 14 2023 at 23:21):
Random Issue Bot said:
Today I chose issue 2724 for discussion!
have
solve_by_elimcallintro1before giving up
Created by Scott Morrison (@semorrison) on 2020-05-18
Labels: help wanted, t-meta, feature-requestIs this issue still relevant? Any recent updates? Anyone making progress?
This was implemented in the mathlib4 version, so I've closed this.
Last updated: Dec 20 2023 at 11:08 UTC