d60c85e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add a default case for addShows

The assumption that the argument lists are equal in length is a flawed one. Fixes #1765

commitd60c85e12c077967a4aef386352413ae78201a92 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 5 Dec 2014, 20:14 (12 years ago) parent6b6aae0

1 file changed+1

unifiedsplit

src/Idris/Delaborate.hs+1

@@ -379,6 +379,7 @@ addImplicitDiffs x y

379379 getTm = b' } : bs')

380380 else (a { getTm = a' } : as',

381381 b { getTm = b' } : bs')

382+ addShows xs ys = (xs, ys)

382383 addI (PLam n a b) (PLam n' c d)

383384 = let (a', c') = addI a c

384385 (b', d') = addI b d in