summaryrefslogtreecommitdiff
path: root/src/Obs/Parser.idr
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2023-01-03 13:46:38 +0000
committerGreg Brown <greg.brown01@ed.ac.uk>2023-01-03 13:46:38 +0000
commit3950a84c00f54ab39f2a209c368cc02460eeebd7 (patch)
treed44712a47db174b42ff545fec1b8c24530f76ce0 /src/Obs/Parser.idr
parentc4bbe4ab5fa5953d468ac1509b37e03aace3085e (diff)
Add more program structure to abstract terms.
Add more program structure to type inference and checking.
Diffstat (limited to 'src/Obs/Parser.idr')
-rw-r--r--src/Obs/Parser.idr3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 8eea42c..68591ee 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -424,7 +424,8 @@ castErr : Either (List1 (ParsingError tok)) a -> Logging ann a
castErr (Right x) = pure x
castErr (Left errs) = do
for_ {b = ()} errs
- (\(Error msg bounds) => maybe id inBounds bounds $ error msg)
+ (\(Error msg bounds) =>
+ inBounds $ map error $ maybe (irrelevantBounds msg) (MkBounded msg True) bounds)
abort
partial