diff options
author | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-03 13:46:38 +0000 |
---|---|---|
committer | Greg Brown <greg.brown01@ed.ac.uk> | 2023-01-03 13:46:38 +0000 |
commit | 3950a84c00f54ab39f2a209c368cc02460eeebd7 (patch) | |
tree | d44712a47db174b42ff545fec1b8c24530f76ce0 /src/Obs/Parser.idr | |
parent | c4bbe4ab5fa5953d468ac1509b37e03aace3085e (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.idr | 3 |
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 |