git.iko.soy/Idris-dev
on master help sign in
Create a proper name supply for identity type

This causes Idris to neither crash nor give an ugly name when proving e.g. transitivity. Fixes #1843.

commitcd30b8e863b903fdf379a040c37aeae56c08ff51 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 11 Jan 2015, 22:40 (12 years ago) parentbf2f3cc
1 file changed+1−1
compare with master
unifiedsplit
src/Idris/CaseSplit.hs+1−1
src/Idris/CaseSplit.hs+1−1
@@ -361,7 +361,7 @@ getClause l fn fp
361361 getNameFrom i used (PPi _ _ _ _)
362362 = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used
363363 getNameFrom i used (PApp fc f as) = getNameFrom i used f
364− getNameFrom i used (PEq _ _ _ _ _) = uniqueNameFrom [sUN "prf"] used
364+ getNameFrom i used (PEq _ _ _ _ _) = uniqueNameFrom (mkSupply [sUN "prf"]) used
365365 getNameFrom i used (PRef fc f)
366366 = case getNameHints i f of
367367 [] -> uniqueName (sUN "x") used