on master help sign in
Fix a few missing lines
7f7af8dBenjamin Saunders
lib/Prelude/Modular.idr+1−1
@@ -33,7 +33,7 @@ modDiv = modBin bitsUDiv
33
33
34public partial
34public partial
35modRem : Mod2 n -> Mod2 n -> Mod2 n
35modRem : Mod2 n -> Mod2 n -> Mod2 n
36−modRem = modBin bitsSDiv
36+modRem = modBin bitsURem
37
37
38%assert_total
38%assert_total
39public
39public
src/Idris/Primitives.hs+1
@@ -580,6 +580,7 @@ intToBits64 [VConstant (I x)] = Just $ toB64 x
580intToBits64 _ = Nothing
580intToBits64 _ = Nothing
581
581
582bits32ToInt [VConstant (B32 x)] = Just $ VConstant (I (fromIntegral x))
582bits32ToInt [VConstant (B32 x)] = Just $ VConstant (I (fromIntegral x))
583+bits32ToInt _ = Nothing
583
584
584c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))
585c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))
585c_intToStr _ = Nothing
586c_intToStr _ = Nothing