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

Merge pull request #96 from ziman/fix-impl-rebuild

Browse Source 
Exclude `DN` from `Hashable Name`
This commit is contained in:
Edwin Brady 2020-05-21 19:20:45 +01:00 committed by GitHub
commit 1e570f5895
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Core/Hash.idr
View File

@ -64,6 +64,8 @@ Hashable String where
export export
Hashable Name where Hashable Name where
hashWithSalt h (MN s _) = hashWithSalt h s hashWithSalt h (MN s _) = hashWithSalt h s
hashWithSalt h (DN _ n) = hashWithSalt h n
hashWithSalt h (NS ns n) = hashWithSalt (hashWithSalt h ns) n
hashWithSalt h (Resolved i) = hashWithSalt h i hashWithSalt h (Resolved i) = hashWithSalt h i
hashWithSalt h n = hashWithSalt h (show n) hashWithSalt h n = hashWithSalt h (show n)