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):
Last updated: May 10 2021 at 19:16 UTC