Hello!
I am skipping around the introduction to ats book and am having fun.
I keep getting stuck on this though from the book:
fun{a:t@ype}
ptr_get0 {l:addr} (pf: a @ l | p: ptr l): (a @ l | a)
>From
http://ats-lang.github.io/DOCUMENT/INT2PROGINATS/HTML/INT2PROGINATS-BOOK-onechunk.html#introduction-to-views-and-viewtypes
I have tried thinking of how to implement this and can't seem to get it
right.
I have tried using the implentation of ptr_get from prelude
SATS:
fun{a:vt0p}
ptr_get{l:addr}
(pf: !INV(a) @ l >> a?! @ l | p: ptr l):<> a
DATS:
implement
{a}(*tmp*)
ptr_get(pf | p) = !p
Obviously those type signatures are different!
Is the ptr_get0 from the introduction implementable?
If so could someone show me an example implementation?
Thanks!
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/b6794984-3062-4d1f-859e-889841a1094b%40googlegroups.com.
