on master help sign in
Conciseness
cbc8a13Benjamin Saunders
lib/Prelude/Modular.idr+1−2
@@ -79,5 +79,4 @@ modToStr x = pack (reverse (helper x))
79 %assert_total
79 %assert_total
80 helper : Mod2 n -> List Char
80 helper : Mod2 n -> List Char
81 helper x = strIndex "0123456789" (unsafeBitsToInt (modToBits (x `modRem` 10)))
81 helper x = strIndex "0123456789" (unsafeBitsToInt (modToBits (x `modRem` 10)))
82− :: (let q = (x `modDiv` 10) in
83− if q == 0 then [] else helper q)
82+ :: (if x < 10 then [] else helper (x `modDiv` 10))