idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-03 00:55:00 +03:00
Code Issues Projects Releases Wiki Activity

Fix error message for LinearMisuse

Browse Source
This commit is contained in:
Justus Matthiesen 2022-06-16 18:22:19 +01:00 committed by G. Allais
parent e5802204b6
commit 1ae4fdd605
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/Core/Core.idr
View File

@ -252,14 +252,14 @@ Show Error where
where
showRig : RigCount -> String
showRig = elimSemi
"linear"
"irrelevant"
"linear"
(const "unrestricted")
showRel : RigCount -> String
showRel = elimSemi
"relevant"
"irrelevant"
"relevant"
(const "non-linear")
show (BorrowPartial fc env t arg)
= show fc ++ ":" ++ show t ++ " borrows argument " ++ show arg ++