idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 02:07:25 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #492 from donovancrichton/pi-type-pattern-match

Browse Source 
Added explicit case to headEq to allow matching on Pi Types.
This commit is contained in:
Niklas Larsson 2020-07-25 11:50:58 +02:00 committed by GitHub
commit eeb1d22234
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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/CaseBuilder.idr
View File

@ -601,6 +601,7 @@ sameType {ns} fc phase fn env (p :: xs)
firstPat (pinf :: _) = pat pinf
headEq : NF ns -> NF ns -> Phase -> Bool
headEq (NBind _ _ (Pi _ _ _) _) (NBind _ _ (Pi _ _ _) _) _ = True
headEq (NTCon _ n _ _ _) (NTCon _ n' _ _ _) _ = n == n'
headEq (NPrimVal _ c) (NPrimVal _ c') _ = c == c'
headEq (NType _) (NType _) _ = True