max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: use noImplicitLambda% when defining tactic macros such as have, let, etc

Browse source 
Thus, we don't change the expected type when using them.
This commit is contained in:
Leonardo de Moura 2021-04-12 23:01:47 -07:00
parent ecad25e08f
commit bf4b9b0ccd
2 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Notation.lean
View file

@ -271,7 +271,7 @@ syntax (name := simpAll) "simp_all " ("(" &"config" " := " term ")")? (&"only ")
-- Auxiliary macro for lifting have/suffices/let/...
-- It makes sure the "continuation" `?_` is the main goal after refining
macro "refineLift " e:term : tactic => `(focus (refine $e; rotateRight))
macro "refineLift " e:term : tactic => `(focus (refine noImplicitLambda% $e; rotateRight))
macro "have " d:haveDecl : tactic => `(refineLift have $d:haveDecl; ?_)
/- We use a priority > default, to avoid ambiguity with previous `have` notation -/
@ -284,7 +284,7 @@ macro_rules
| `(tactic| let rec $d:letRecDecls) => `(tactic| refineLift let rec $d:letRecDecls; ?_)
-- Similar to `refineLift`, but using `refine'`
macro "refineLift' " e:term : tactic => `(focus (refine' $e; rotateRight))
macro "refineLift' " e:term : tactic => `(focus (refine' noImplicitLambda% $e; rotateRight))
macro "have' " d:haveDecl : tactic => `(refineLift' have $d:haveDecl; ?_)
macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x:ident : _ := $p)
macro "let' " d:letDecl : tactic => `(refineLift' let $d:letDecl; ?_)

2
tests/lean/run/impLambdaTac.lean
View file

@ -26,8 +26,6 @@ example (P : Prop) : ∀ {p : P}, P := by
refine noImplicitLambda% (have _ from 1; ?_)
apply id
#exit
-- After update stage0, we fix this
example (P : Prop) : ∀ {p : P}, P := by
have _ from 1
apply id