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_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?

This was implemented in the mathlib4 version, so I've closed this.


Last updated: Dec 20 2023 at 11:08 UTC