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

Ignore DN layers in Hashable Name.

Browse Source 
So that hashes do not depend on irrelevant information,
such as line/column numbers of interface implementations.
This commit is contained in:
Matus Tejiscak 2020-05-21 17:30:27 +02:00
parent 8291c8bbeb
commit b39f1fd161
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
Hashable Name where
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 n = hashWithSalt h (show n)