Zulip Chat Archive

Stream: general

Topic: request


Scott Morrison (Oct 01 2018 at 13:03):

Hi @Johannes Hölzl, @Mario Carneiro, I'm hoping one of you can have a look at <https://github.com/leanprover/mathlib/pull/382> for me. (It's a replacement for https://github.com/leanprover/mathlib/pull/324, which has been up for a few weeks; I cleaned up the history and left the previous discussion at the old PR.)

I need to build further on this PR in order to build one more tactic before I can continue migrating my category theory library (limits and colimits), but I'd like to be sure this first PR is okay.

Scott Morrison (Oct 01 2018 at 13:04):

This PR just extends the syntax of solve_by_elim, allowing the user at add or remove additional lemmas or hypotheses from the set of lemmas that are applied.


Last updated: Dec 20 2023 at 11:08 UTC