Zulip Chat Archive

Stream: new members

Topic: adding hypothesis from lemma

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?

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.

Peter Nelson (Aug 14 2020 at 18:07):

Thank you!

Last updated: Dec 20 2023 at 11:08 UTC