Zulip Chat Archive

Stream: new members

Topic: adding hypothesis from lemma


view this post on Zulip Peter Nelson (Aug 14 2020 at 18:02):

If I am in tactic mode and there is a lemma (foo a b ) elsewhere, is there a way to add (foo a b) directly to my hypotheses without using 'have' and retyping the full statement of foo?

view this post on Zulip Reid Barton (Aug 14 2020 at 18:05):

have h := foo a b, or have := foo a b. You don't have to give the type if you don't want to.

view this post on Zulip Peter Nelson (Aug 14 2020 at 18:07):

Thank you!


Last updated: May 10 2021 at 19:16 UTC