Stream: new members
Michael Beeson (Sep 05 2020 at 15:40):
Suppose I have already proved lemma23: \all x (p -> q) for some complicated p and q containing x,
and in my current proof state I have h:p[x:= t], so I would like to have Lean generate for me
have h3: q[x:t] := lemma23 x h
without me having to type out q[x:=t], I just want to say, "use lemma23 on h" and have
the new hypothesis appear.
Is there any way to do that?
Bryan Gin-ge Chen (Sep 05 2020 at 15:42):
If I understand what you're asking, type ascriptions are usually optional, so
have h3 := lemma23 x h should work as well.
Michael Beeson (Sep 05 2020 at 15:42):
Oh! Well, that was easy! Thanks.
Last updated: May 17 2021 at 22:15 UTC