Paste: memcpy in ATS

Author: doublec
Mode: maple
Date: Fri, 26 Nov 2010 03:57:33
Plain Text | 
fun memcpy {n:nat}
  {n1,n2:nat | n <= n1; n <= n2} {l:addr} (
    pf_dst: !bytes n1 @ l | p_dst: ptr l, p_src: &bytes n2, n: size_t n
  ) :<> ptr l = "atslib_memcpy"
// end of [memcpy]

New Annotation

Summary:
Author:
Mode:
Body: