Zulip Chat Archive

Stream: general

Topic: linarith and conjunctions


view this post on Zulip Patrick Massot (Apr 03 2020 at 15:06):

In my class I got tired of typing cases h with h1 h2, cases ..., cases ..., linarith all the time and ended up defining

meta def linarith' : tactic unit :=
do try auto.split_hyps,
       `[linarith]

@Rob Lewis Would you mind putting (a more flexible version of) this in mathlib?

view this post on Zulip Rob Lewis (Apr 03 2020 at 15:39):

https://github.com/leanprover-community/mathlib/pull/2320

view this post on Zulip Patrick Massot (Apr 03 2020 at 15:41):

Thanks!


Last updated: May 09 2021 at 19:11 UTC