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

Don't look inside guesses for metavariables

Browse Source 
This will happen if there's an error earlier in the file, and only leads
to a cryptic error message
This commit is contained in:
Edwin Brady 2019-07-04 10:54:01 +01:00
parent 6f5d3f5fef
commit 4f4be770ad
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/Core/LinearCheck.idr
View File

@ -206,6 +206,7 @@ mutual
| _ => throw (UndefinedName fc n) | _ => throw (UndefinedName fc n)
let expand = case (definition gdef, rig) of let expand = case (definition gdef, rig) of
(Hole _ _, _) => False (Hole _ _, _) => False
(Guess _ _, _) => False
(_, Rig0) => False (_, Rig0) => False
_ => True _ => True
if expand if expand