git.iko.soy/Idris-dev
on master help sign in
Add Cast instance for String to Nat
d579d27Edwin Brady
libs/prelude/Prelude/Nat.idr+3
compare with master
unifiedsplit
@@ -214,6 +214,9 @@ instance MinBound Nat where
214instance Cast Integer Nat where
214instance Cast Integer Nat where
215 cast = fromInteger
215 cast = fromInteger
216
216
217+instance Cast String Nat where
218+ cast str = cast (the Integer (cast str))
219+
217||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)
220||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)
218record Multiplicative where
221record Multiplicative where
219 constructor GetMultiplicative
222 constructor GetMultiplicative
test/proofsearch002/proofsearch002.idr−3
@@ -24,9 +24,6 @@ mathsServer = do Lift $ putStrLn "Serving maths!"
24 Pure (fact k, ()))
24 Pure (fact k, ()))
25 Loop mathsServer
25 Loop mathsServer
26
26
27−instance Cast String Nat where
28− cast orig = cast (the Integer (cast orig))
29−
30-- Start up a couple of servers, send them requests
27-- Start up a couple of servers, send them requests
31testProg1 : Program () (const Void)
28testProg1 : Program () (const Void)
32testProg1 = do -- with Process do
29testProg1 = do -- with Process do