@@ -354,11 +354,11 @@ Integral Int where
354-- ------------------------------------------------------------------- [ Bits8 ]
354-- ------------------------------------------------------------------- [ Bits8 ]
355divB8 : Bits8 -> Bits8 -> Bits8
355divB8 : Bits8 -> Bits8 -> Bits8
356divB8 x y = case y == 0 of
356divB8 x y = case y == 0 of
357− False => prim__sdivB8 x y
357+ False => prim__udivB8 x y
359modB8 : Bits8 -> Bits8 -> Bits8
359modB8 : Bits8 -> Bits8 -> Bits8
360modB8 x y = case y == 0 of
360modB8 x y = case y == 0 of
361− False => prim__sremB8 x y
361+ False => prim__uremB8 x y
363Integral Bits8 where
363Integral Bits8 where
364 div = divB8
364 div = divB8
@@ -367,11 +367,11 @@ Integral Bits8 where
367-- ------------------------------------------------------------------ [ Bits16 ]
367-- ------------------------------------------------------------------ [ Bits16 ]
368divB16 : Bits16 -> Bits16 -> Bits16
368divB16 : Bits16 -> Bits16 -> Bits16
369divB16 x y = case y == 0 of
369divB16 x y = case y == 0 of
370− False => prim__sdivB16 x y
370+ False => prim__udivB16 x y
372modB16 : Bits16 -> Bits16 -> Bits16
372modB16 : Bits16 -> Bits16 -> Bits16
373modB16 x y = case y == 0 of
373modB16 x y = case y == 0 of
374− False => prim__sremB16 x y
374+ False => prim__uremB16 x y
376Integral Bits16 where
376Integral Bits16 where
377 div = divB16
377 div = divB16
@@ -380,11 +380,11 @@ Integral Bits16 where
380-- ------------------------------------------------------------------ [ Bits32 ]
380-- ------------------------------------------------------------------ [ Bits32 ]
381divB32 : Bits32 -> Bits32 -> Bits32
381divB32 : Bits32 -> Bits32 -> Bits32
382divB32 x y = case y == 0 of
382divB32 x y = case y == 0 of
383− False => prim__sdivB32 x y
383+ False => prim__udivB32 x y
385modB32 : Bits32 -> Bits32 -> Bits32
385modB32 : Bits32 -> Bits32 -> Bits32
386modB32 x y = case y == 0 of
386modB32 x y = case y == 0 of
387− False => prim__sremB32 x y
387+ False => prim__uremB32 x y
389Integral Bits32 where
389Integral Bits32 where
390 div = divB32
390 div = divB32
@@ -393,11 +393,11 @@ Integral Bits32 where
393-- ------------------------------------------------------------------ [ Bits64 ]
393-- ------------------------------------------------------------------ [ Bits64 ]
394divB64 : Bits64 -> Bits64 -> Bits64
394divB64 : Bits64 -> Bits64 -> Bits64
395divB64 x y = case y == 0 of
395divB64 x y = case y == 0 of
396− False => prim__sdivB64 x y
396+ False => prim__udivB64 x y
398modB64 : Bits64 -> Bits64 -> Bits64
398modB64 : Bits64 -> Bits64 -> Bits64
399modB64 x y = case y == 0 of
399modB64 x y = case y == 0 of
400− False => prim__sremB64 x y
400+ False => prim__uremB64 x y
402Integral Bits64 where
402Integral Bits64 where
403 div = divB64
403 div = divB64