From bf4b9b0ccd7688d3d4024bc06a0c7a3b207124bd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 12 Apr 2021 23:01:47 -0700 Subject: [PATCH] fix: use `noImplicitLambda%` when defining tactic macros such as `have`, `let`, etc Thus, we don't change the expected type when using them. --- src/Init/Notation.lean | 4 ++-- tests/lean/run/impLambdaTac.lean | 2 -- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 71bd756ec6..6d6be5fe53 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -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; ?_) diff --git a/tests/lean/run/impLambdaTac.lean b/tests/lean/run/impLambdaTac.lean index 0dfef87b67..721dcec937 100644 --- a/tests/lean/run/impLambdaTac.lean +++ b/tests/lean/run/impLambdaTac.lean @@ -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