From f37b700e6ef230fd49974704c52fed8a54b00906 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Wed, 27 Apr 2022 00:55:27 -0700 Subject: [PATCH] fix: use correct number of `none` patterns for antiquotation splice --- src/Lean/Elab/Quotation.lean | 2 +- tests/lean/run/1124.lean | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/1124.lean diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index f50d14cb67..35ff8dbce7 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -131,7 +131,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax let arr ← match k with | `optional => `(match $[$ids:ident],* with | $[some $ids:ident],* => $(quote inner) - | none => Array.empty) + | $[_%$ids],* => Array.empty) | _ => let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id $arr)) ids.back `(Array.map (fun $(← mkTuple ids) => $(inner[0])) $arr) diff --git a/tests/lean/run/1124.lean b/tests/lean/run/1124.lean new file mode 100644 index 0000000000..a344a16aa1 --- /dev/null +++ b/tests/lean/run/1124.lean @@ -0,0 +1,5 @@ +open Lean +syntax "foo" (ident ident)? : term + +variable (x y : Option Syntax) +example : MacroM Syntax := `(foo $[$x:ident $y:ident]?)