Zulip Chat Archive

Stream: new members

Topic: tactic wishlist?


Patrick Thomas (Sep 29 2020 at 01:36):

I am starting to look at tactic writing and I am looking for ideas for tactics to write that might be useful. Is there a wishlist or something similar somewhere?

Yury G. Kudryashov (Sep 29 2020 at 01:43):

It would be nice to have a way to tag the lemma docs#real.has_deriv_at_cos with some attribute and have Lean define the next few lemmas in the file (has_deriv_within_at, continuous_at, diferentiable_at, differentiable, continuous, deriv, deriv_within). Or have a command that generates standard lemmas about equivs like docs#equiv.surjective or docs#equiv.apply_eq_iff_eq_symm_apply for a new equivalence (e.g., docs#linear_equiv) using proofs like linear_equiv.to_equiv.apply_symm_apply.

Yury G. Kudryashov (Sep 29 2020 at 01:44):

(this is (a part of) my personal wish list)

Bryan Gin-ge Chen (Sep 29 2020 at 02:01):

There are a bunch of requests in mathlib's issues.

Bryan Gin-ge Chen (Sep 29 2020 at 02:04):

Oh, there's a thread in the general stream too.

Patrick Thomas (Sep 29 2020 at 02:07):

Bryan Gin-ge Chen said:

Oh, there's a thread in the general stream too.

Oops.

Patrick Thomas (Sep 29 2020 at 02:08):

Thank you.


Last updated: Dec 20 2023 at 11:08 UTC