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

feat: $. notation

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-19 14:03:27 -08:00
parent f04f51a295
commit e221a239f8
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Parser/Term.lean
View file

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