edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-18 10:21:39 +03:00
Code Issues Projects Releases Wiki Activity

Fix record dot syntax parser.

Browse Source
This commit is contained in:
Matus Tejiscak 2020-04-17 00:35:39 +02:00
parent ca1ef8a882
commit 4b986e8b61
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/Idris/Parser.idr
View File

@ -314,7 +314,7 @@ mutual
simpleExpr fname indents = simpleExpr fname indents =
do do
start <- location start <- location
recFields <- many recField recFields <- some recField
end <- location end <- location
pure $ PRecordProjection (MkFC fname start end) recFields pure $ PRecordProjection (MkFC fname start end) recFields
<|> do <|> do
@ -322,7 +322,7 @@ mutual
root <- simplerExpr fname indents root <- simplerExpr fname indents
recFields <- many recField recFields <- many recField
end <- location end <- location
case recFields of pure $ case recFields of
[] => root [] => root
fs => PRecordFieldAccess (MkFC fname start end) root recFields fs => PRecordFieldAccess (MkFC fname start end) root recFields