git.iko.soy/Idris-dev
on master help sign in
Another intercommit.
e5b7866Matus Tejiscak
src/Idris/Erasure.hs+1−1
compare with master
unifiedsplit
@@ -101,7 +101,7 @@ buildDepGraph ctx cg = unionMap (findDepsDef cg <*> getDef ctx)
101 , findDepsTerm cg vars (tn,ta) (binderTy b)
101 , findDepsTerm cg vars (tn,ta) (binderTy b)
102 ]
102 ]
103
103
104− infixr 3 (~>)
104+ infixr 3 ~>
105 (~>) :: (Ord a) => a -> b -> Map a b
105 (~>) :: (Ord a) => a -> b -> Map a b
106 (~>) = M.singleton
106 (~>) = M.singleton
107
107
src/Idris/IBC.hs+3−3
@@ -177,9 +177,9 @@ ibc i (IBCDef n) f
177
177
178 updateSC (Case n alts) = do alts' <- mapM updateAlt alts
178 updateSC (Case n alts) = do alts' <- mapM updateAlt alts
179 return (Case n alts')
179 return (Case n alts')
180− updateSC (ProjCase t alts) = do t' <- update t
180+ updateSC (ProjCase t alt) = do t' <- update t
181− alts' <- mapM updateAlt alts
181+ alt' <- updateAlt alt
182− return (ProjCase t' alts')
182+ return (ProjCase t' alt')
183 updateSC (STerm t) = do t' <- update t
183 updateSC (STerm t) = do t' <- update t
184 return (STerm t')
184 return (STerm t')
185 updateSC t = return t
185 updateSC t = return t