From f2ca5db169423a133487bfceefe110ad7a6b5351 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Aug 2019 15:20:47 -0700 Subject: [PATCH] chore(library/init/lean/parser/term): remove support for Lean3 syntax --- library/init/lean/parser/term.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index 5c81a3ca37..e4dd82afeb 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -98,8 +98,7 @@ def matchAlt := parser! " | " >> sepBy1 termParser ", " >> unicodeSymbol "⇒" " /- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/ def letIdLhs : Parser := ident >> checkWsBefore "expected space before binders" >> many bracktedBinder >> optType def letIdDecl := parser! try (letIdLhs >> " := ") >> termParser -def equation3 := parser! try (" | " >> many1 (termParser appPrec) >> " := ") >> termParser -- Lean3 equation -def equation := equation3 <|> matchAlt +def equation := matchAlt def letEqns := parser! try (letIdLhs >> lookahead " | ") >> many1Indent equation "equations must be indented" def letPatDecl := parser! termParser >> optType >> " := " >> termParser def letDecl := try letIdDecl <|> letEqns <|> letPatDecl