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

chore: remove unnecessary partial

Browse source 
TODO: we should generate an error/warning when `partial` is not necessary
This commit is contained in:
Leonardo de Moura 2022-02-15 12:16:49 -08:00
parent a2613a36a4
commit e07823bb12
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Quotation/Util.lean
View file

@ -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