git.iko.soy/Idris-dev
on master help sign in
Made do_poke private
b6effdbJan Bessai
effects/Effect/Memory.idr+1
compare with master
unifiedsplit
@@ -58,6 +58,7 @@ do_peek ptr offset (S n)
58 bs <- do_peek ptr (S offset) n
58 bs <- do_peek ptr (S offset) n
59 Prelude.Monad.return (Prelude.Vect.(::) (prim__intToB8 b) bs)
59 Prelude.Monad.return (Prelude.Vect.(::) (prim__intToB8 b) bs)
60
60
61+private
61do_poke : Ptr -> Nat -> Vect Bits8 size -> IO ()
62do_poke : Ptr -> Nat -> Vect Bits8 size -> IO ()
62do_poke _ _ [] = return ()
63do_poke _ _ [] = return ()
63do_poke ptr offset (b::bs)
64do_poke ptr offset (b::bs)