Add iso between String and List Char
commit2159801579ee1450aec96e6b50940d7ca7904017
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateTue 4 Feb 2014, 09:08 (13 years ago)
parent626d0ea
libs/base/Control/Isomorphism/Primitives.idr+8
@@ -25,3 +25,11 @@ integerIsoZZ = MkIso toZZ fromZZ fromToZZ toFromZZ
2525 fromToZZ : (n : ZZ) -> toZZ (fromZZ n) = n
2626 fromToZZ n = really_believe_me {a = n=n} {b = toZZ (fromZZ n) = n} refl
2727
28+
29+packUnpackIso : Iso (List Char) String
30+packUnpackIso = MkIso pack
31+ unpack
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)
34+
35+