From d27770ea0e86c2dd202d918f8b6f54ff4acbd8d5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 5 Dec 2020 15:36:23 -0800 Subject: [PATCH] chore: prepare to add `scoped` and `local` instances --- src/Lean/Parser/Command.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index d9f7bea495..1e949d2878 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -42,7 +42,10 @@ def «abbrev» := parser! "abbrev " >> declId >> optDeclSig >> declVal def «def» := parser! "def " >> declId >> optDeclSig >> declVal def «theorem» := parser! "theorem " >> declId >> declSig >> declVal def «constant» := parser! "constant " >> declId >> declSig >> optional declValSimple -def «instance» := parser! "instance " >> optional declId >> declSig >> declVal +def «instance» := parser! + (checkOutsideQuot >> "instance " >> optional declId >> declSig >> declVal) + <|> + (checkInsideQuot >> Term.attrKind >> "instance " >> optional declId >> declSig >> declVal) def «axiom» := parser! "axiom " >> declId >> declSig def «example» := parser! "example " >> declSig >> declVal def inferMod := parser! atomic (symbol "{" >> "}")