From e07823bb12fc0472712645e75a3712e8e71f8600 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 15 Feb 2022 12:16:49 -0800 Subject: [PATCH] chore: remove unnecessary `partial` TODO: we should generate an error/warning when `partial` is not necessary --- src/Lean/Elab/Quotation/Util.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Elab/Quotation/Util.lean b/src/Lean/Elab/Quotation/Util.lean index 74e5e50946..dffcf14079 100644 --- a/src/Lean/Elab/Quotation/Util.lean +++ b/src/Lean/Elab/Quotation/Util.lean @@ -13,7 +13,7 @@ register_builtin_option hygiene : Bool := { descr := "Annotate identifiers in quotations such that they are resolved relative to the scope at their declaration, not that at their eventual use/expansion, to avoid accidental capturing. Note that quotations/notations already defined are unaffected." } -partial def getAntiquotationIds (stx : Syntax) : TermElabM (Array Syntax) := do +def getAntiquotationIds (stx : Syntax) : TermElabM (Array Syntax) := do let mut ids := #[] for stx in stx.topDown do if (isAntiquot stx || isTokenAntiquot stx) && !isEscapedAntiquot stx then