On Friday, January 5, 2018 at 6:26:59 PM UTC+6, Chris Double wrote: > > With the following code: > > fun test {l:agz}(pf: !array_v(int, l, 2)| p: ptr l): void = let > prval (pf_x, pf_xs) = array_v_uncons(pf) > prval (pf_x1, pf_xs1) = array_v_uncons(pf_xs) > val () = !p := 0 > val p2 = ptr1_succ<int>(p) > val () = !p2 := 0 > prval () = pf_xs := array_v_cons(pf_x1, pf_xs1) > prval () = pf := array_v_cons(pf_x, pf_xs) > in () end > > I get an error in the "!p2 := 0" line saying it can't find the proof > search for the assignment to 'p2' failed. Shouldn't that be the 'pf_1' > proof? What am I doing wrong? > > While I can't answer your question, this works:
https://glot.io/snippets/ex2t763amv (I guess you're well aware it would have worked, but I decided to post it nevertheless. This style is clumsy/difficult to follow, but it works.) > -- > http://bluishcoder.co.nz > -- 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 ats-lang-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. 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/0a441d7e-b868-4208-b6e4-534f03e19496%40googlegroups.com.