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

chore(library/init/lean/parser/term): remove support for Lean3 syntax

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-13 15:20:47 -07:00
parent cbcf2a8a49
commit f2ca5db169
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/lean/parser/term.lean
View file

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