I took a look at the source code of the typechecker.
There was a missing case. Now this issue has been fixed.
Changes will go into the next release. Thanks!
On Friday, January 5, 2018 at 7:26:59 AM UTC-5, 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?
>
> --
> 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/027e2f8a-6aa5-439c-bc95-717d53f50160%40googlegroups.com.
