From 55bb8e905aba4e3c6db382c9a4268e4b986c13f8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Aug 2022 21:09:16 -0700 Subject: [PATCH] chore: `binderIdent` normalization fixes #1411 --- src/Init/Data/Nat/Linear.lean | 2 +- src/Init/Tactics.lean | 8 ++++---- src/Lean/Elab/PreDefinition/WF/TerminationHint.lean | 2 +- src/Lean/Elab/Tactic/Induction.lean | 2 +- src/Lean/Parser/Command.lean | 2 +- tests/lean/run/1411.lean | 6 ++++++ 6 files changed, 14 insertions(+), 8 deletions(-) create mode 100644 tests/lean/run/1411.lean diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean index 9115fbf392..76d097abb3 100644 --- a/src/Init/Data/Nat/Linear.lean +++ b/src/Init/Data/Nat/Linear.lean @@ -338,7 +338,7 @@ theorem Poly.denote_mul (ctx : Context) (k : Nat) (p : Poly) : (p.mul k).denote by_cases h : k == 1 <;> simp [h]; simp [eq_of_beq h] induction p with | nil => simp - | cons kv m ih => cases kv with | _ k' v => simp [ih] + | cons kv m ih => cases kv with | mk k' v => simp [ih] private theorem eq_of_not_blt_eq_true (h₁ : ¬ (Nat.blt x y = true)) (h₂ : ¬ (Nat.blt y x = true)) : x = y := have h₁ : ¬ x < y := fun h => h₁ (Nat.blt_eq.mpr h) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 923e8934f9..6ef7679e0d 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -8,7 +8,7 @@ import Init.Notation namespace Lean -syntax binderIdent := ident <|> "_" +syntax binderIdent := ident <|> hole namespace Parser.Tactic /-- `with_annotate_state stx t` annotates the lexical range of `stx : Syntax` with the initial and final state of running tactic `t`. -/ @@ -34,7 +34,7 @@ For each hypothesis to be introduced, the remaining main goal's target type must -/ syntax (name := intro) "intro " notFollowedBy("|") (colGt term:max)* : tactic /-- `intros x...` behaves like `intro x...`, but then keeps introducing (anonymous) hypotheses until goal is not of a function type. -/ -syntax (name := intros) "intros " (colGt (ident <|> "_"))* : tactic +syntax (name := intros) "intros " (colGt (ident <|> hole))* : tactic /-- `rename t => x` renames the most recent hypothesis whose type matches `t` (which may contain placeholders) to `x`, or fails if no such hypothesis could be found. -/ @@ -253,7 +253,7 @@ should be constructor applications of the same constructor. Given `h : a::b = c::d`, the tactic `injection h` adds two new hypothesis with types `a = c` and `b = d` to the main goal. The tactic `injection h with h₁ h₂` uses the names `h₁` and `h₂` to name the new hypotheses. -/ -syntax (name := injection) "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic +syntax (name := injection) "injection " term (" with " (colGt (ident <|> hole))+)? : tactic /-- `injections` applies `injection` to all hypotheses recursively (since `injection` can produce new hypotheses). Useful for destructing nested @@ -354,7 +354,7 @@ macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x : /-- Similar to `let`, but using `refine'` -/ macro "let' " d:letDecl : tactic => `(refine_lift' let $d:letDecl; ?_) -syntax inductionAltLHS := "| " (("@"? ident) <|> "_") (ident <|> "_")* +syntax inductionAltLHS := "| " (("@"? ident) <|> hole) (ident <|> hole)* syntax inductionAlt := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> syntheticHole <|> tacticSeq) syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+) /-- diff --git a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean index ec13ac67c5..2538b86a97 100644 --- a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean +++ b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean @@ -98,7 +98,7 @@ inductive TerminationWF where /- ``` -def terminationByElement := leading_parser ppLine >> (ident <|> "_") >> many (ident <|> "_") >> " => " >> termParser >> optional ";" +def terminationByElement := leading_parser ppLine >> (ident <|> hole) >> many (ident <|> hole) >> " => " >> termParser >> optional ";" def terminationBy := leading_parser ppLine >> "termination_by " >> many1chIndent terminationByElement ``` -/ diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 249c338cdf..a12d48cb4c 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -21,7 +21,7 @@ open Meta /- Given an `inductionAlt` of the form ``` - syntax inductionAltLHS := "| " (group("@"? ident) <|> "_") (ident <|> "_")* + syntax inductionAltLHS := "| " (group("@"? ident) <|> hole) (ident <|> hole)* syntax inductionAlt := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> syntheticHole <|> tacticSeq) ``` -/ diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 10b887e78c..6f52e4ec62 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -35,7 +35,7 @@ def terminationHint (p : Parser) := terminationHintMany p <|> terminationHint1 p def terminationByCore := leading_parser "termination_by' " >> terminationHint termParser def decreasingBy := leading_parser "decreasing_by " >> terminationHint Tactic.tacticSeq -def terminationByElement := leading_parser ppLine >> (ident <|> "_") >> many (ident <|> "_") >> " => " >> termParser >> optional ";" +def terminationByElement := leading_parser ppLine >> (ident <|> Term.hole) >> many (ident <|> Term.hole) >> " => " >> termParser >> optional ";" def terminationBy := leading_parser ppLine >> "termination_by " >> many1Indent terminationByElement def terminationSuffix := optional (terminationBy <|> terminationByCore) >> optional decreasingBy diff --git a/tests/lean/run/1411.lean b/tests/lean/run/1411.lean new file mode 100644 index 0000000000..6800f1a8d7 --- /dev/null +++ b/tests/lean/run/1411.lean @@ -0,0 +1,6 @@ +namespace Lean +syntax "foo " binderIdent : term +example : Syntax → MacroM Syntax + | `(foo _) => `(_) + | `(foo $x:ident) => `($x:ident) + | _ => `(_)