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

Fix unification error

Browse Source 
A typo! But it causes some things to fail to unify, especially in proof
search.
This commit is contained in:
Edwin Brady 2020-08-04 20:53:01 +01:00
parent 3c601d9878
commit 663f895058
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Core/Unify.idr
View File

@ -764,7 +764,7 @@ mutual
unifyHoleApp swap mode loc env mname mref margs margs' (NDCon nfc n t a args')
= do defs <- get Ctxt
mty <- lookupTyExact n (gamma defs)
unifyInvertible swap (lower mode) loc env mname mref margs margs' mty (NTCon nfc n t a) args'
unifyInvertible swap (lower mode) loc env mname mref margs margs' mty (NDCon nfc n t a) args'
unifyHoleApp swap mode loc env mname mref margs margs' (NApp nfc (NLocal r idx p) args')
= unifyInvertible swap (lower mode) loc env mname mref margs margs' Nothing
(NApp nfc (NLocal r idx p)) args'