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

Fix typo.

Browse Source
This commit is contained in:
Matus Tejiscak 2020-05-22 00:04:25 +02:00
parent 8ed8ee463e
commit 1e968c14cf
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/Context.idr
View File

@ -1185,7 +1185,7 @@ prettyName (NS ns n) = prettyName n
prettyName n = pure (show n)
-- Add a hash of a thing that contains names,
-- but convert the internal numbers to full numbers first.
-- but convert the internal numbers to full names first.
-- This makes the hash not depend on the internal numbering,
-- which is unstable.
export