@@ -25,3 +25,11 @@ integerIsoZZ = MkIso toZZ fromZZ fromToZZ toFromZZ
25 fromToZZ : (n : ZZ) -> toZZ (fromZZ n) = n
25 fromToZZ : (n : ZZ) -> toZZ (fromZZ n) = n
26 fromToZZ n = really_believe_me {a = n=n} {b = toZZ (fromZZ n) = n} refl
26 fromToZZ n = really_believe_me {a = n=n} {b = toZZ (fromZZ n) = n} refl
29+packUnpackIso : Iso (List Char) String
30+packUnpackIso = MkIso pack
32+ (\str => really_believe_me {a = str=str} {b = pack (unpack str) = str} refl)
33+ (\cs => really_believe_me {a = cs=cs} {b = unpack (pack cs) = cs} refl)