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

chore: remove old syntax

Browse source
This commit is contained in:
Sebastian Ullrich 2020-08-19 13:21:51 +02:00 • committed by Leonardo de Moura
parent 14ef490aa0
commit 6cbfe2359b
2 changed files with 6 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Parser/Level.lean
View file

@ -21,8 +21,8 @@ namespace Level
@[builtinLevelParser] def max := parser! nonReservedSymbol "max " true >> many1 (levelParser maxPrec)
@[builtinLevelParser] def imax := parser! nonReservedSymbol "imax " true >> many1 (levelParser maxPrec)
@[builtinLevelParser] def hole := parser! "_"
@[builtinLevelParser] def num := checkInsideQuot >> numLit <|> checkOutsideQuot >> parser! numLit
@[builtinLevelParser] def ident := checkInsideQuot >> ident <|> checkOutsideQuot >> parser! ident
@[builtinLevelParser] def num := numLit
@[builtinLevelParser] def ident := ident
@[builtinLevelParser] def addLit := tparser!:65 "+" >> numLit
end Level

11
src/Lean/Parser/Term.lean
View file

@ -43,13 +43,10 @@ checkPrec prec >> symbol sym >> termParser (prec+1)
def leadPrec := maxPrec - 1
/- Built-in parsers -/
def explicitUniv' := checkNoWsBefore "no space before '.{'" >> parser! ".{" >> sepBy1 levelParser ", " >> "}"
def namedPattern' := checkNoWsBefore "no space before '@'" >> parser! "@" >> termParser maxPrec
@[builtinTermParser] def id := checkOutsideQuot >> parser! ident >> optional (explicitUniv' <|> namedPattern')
@[builtinTermParser] def ident := checkInsideQuot >> Parser.ident
@[builtinTermParser] def num : Parser := checkInsideQuot >> numLit <|> checkOutsideQuot >> parser! numLit
@[builtinTermParser] def str : Parser := checkInsideQuot >> strLit <|> checkOutsideQuot >> parser! strLit
@[builtinTermParser] def char : Parser := checkInsideQuot >> charLit <|> checkOutsideQuot >> parser! charLit
@[builtinTermParser] def ident := Parser.ident
@[builtinTermParser] def num : Parser := numLit
@[builtinTermParser] def str : Parser := strLit
@[builtinTermParser] def char : Parser := charLit
@[builtinTermParser] def type := parser! "Type" >> optional (checkWsBefore "" >> checkPrec (maxPrec-1) >> levelParser maxPrec)
@[builtinTermParser] def sort := parser! "Sort" >> optional (checkWsBefore "" >> checkPrec (maxPrec-1) >> levelParser maxPrec)
@[builtinTermParser] def prop := parser! "Prop"