Okay so binding has nothing to do with proof consumption then? Maybe I understand now lol.
On Tuesday, December 11, 2018 at 8:13:09 PM UTC-6, gmhwxi wrote: > > >>(pf | !p) > > This does not work because type-checking is performed from > left to right. So you need > > let val x = !p in (pf | x) end > > > On Tue, Dec 11, 2018 at 6:57 PM Scott Murphy <[email protected] > <javascript:>> wrote: > >> Thank you so much. >> So the binding with val A is what forces pf to be considered >> consumed. >> >> I have tried: >> fun{a:t@ype} >> ptr_get0 {l:addr} (pf: a @ l | p: ptr l): (a @ l | a) = (pf|!p) >> and seen the consumption error so many times but wasn't sure exactly what >> consumption meant! >> >> >> >> On Tuesday, December 11, 2018 at 4:41:24 PM UTC-6, Richard wrote: >>> >>> Not sure if this is completely correct however, it typechecks >>> >>> extern fun {a:t@ype} >>> ptr_get0 {l:addr} (pf: a @ l | p: ptr l): (a @ l | a) >>> >>> implement {a} ptr_get0 {l} (pf | p) = (pf | A) where { val A = !p } >>> >>> -- >> 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] <javascript:>. >> To post to this group, send email to [email protected] >> <javascript:>. >> 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/9689d6a2-2dfb-4110-b8e1-c8e616b35696%40googlegroups.com >> >> <https://groups.google.com/d/msgid/ats-lang-users/9689d6a2-2dfb-4110-b8e1-c8e616b35696%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- 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/3f188543-4655-42ca-8696-bb371641172f%40googlegroups.com.
