From e221a239f8846e4fa3182c218ab43ec47f1b2c13 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Dec 2019 14:03:27 -0800 Subject: [PATCH] feat: `$.` notation --- src/Init/Lean/Parser/Term.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean index 12a39129f8..1d6845f91c 100644 --- a/src/Init/Lean/Parser/Term.lean +++ b/src/Init/Lean/Parser/Term.lean @@ -143,6 +143,8 @@ def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Te @[builtinTermParser] def arrayRef := tparser! pushLeading >> symbolNoWs "[" (appPrec+1) >> termParser >>"]" @[builtinTermParser] def dollar := tparser! try (pushLeading >> dollarSymbol >> checkWsBefore "space expected") >> termParser 0 +@[builtinTermParser] def dollarProj := tparser! pushLeading >> symbol "$." 1 >> (fieldIdx <|> ident) + @[builtinTermParser] def fcomp := tparser! infixR " ∘ " 90 @[builtinTermParser] def prod := tparser! infixR " × " 35