649b340 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add with expressions to IBC files

This prevents the following error: idris: src/Idris/IBC.hs:(1546,13)-(1652,44): Non-exhaustive patterns in case

commit649b340f1724b31e89d8055f4276c99eb0b583f5 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 5 Feb 2014, 09:00 (13 years ago) parenta83671e

1 file changed+8−1

compare with master

unifiedsplit

src/Idris/IBC.hs+8−1

src/Idris/IBC.hs+8−1

@@ -26,7 +26,7 @@ import Util.Zlib (decompressEither)

2626

2727

2828ibcVersion :: Word8

29−ibcVersion = 58

29+ibcVersion = 59

3030

3131

3232data IBCFile = IBCFile { ver :: Word8,

@@ -1650,6 +1650,10 @@ instance Binary PTerm where

16501650 put x1

16511651 PNoImplicits x1 -> do putWord8 36

16521652 put x1

1653+ PDisamb x1 x2 -> do putWord8 37

1654+ put x1

1655+ put x2

1656+

16531657 get

16541658 = do i <- getWord8

16551659 case i of

@@ -1759,6 +1763,9 @@ instance Binary PTerm where

17591763 return (PUnifyLog x1)

17601764 36 -> do x1 <- get

17611765 return (PNoImplicits x1)

1766+ 37 -> do x1 <- get

1767+ x2 <- get

1768+ return (PDisamb x1 x2)

17621769 _ -> error "Corrupted binary data for PTerm"

17631770

17641771instance (Binary t) => Binary (PTactic' t) where