thank you! On Wednesday, December 12, 2018 at 2:16:21 PM UTC-6, gmhwxi wrote: > > 'kept' : pf is held by the type-checker and no longer available when '!p' > is type-checked. > > On Wed, Dec 12, 2018 at 3:13 PM Scott Murphy <[email protected] > <javascript:>> wrote: > >> What is meant by kept? >> >> On Wednesday, December 12, 2018 at 9:47:33 AM UTC-6, gmhwxi wrote: >>> >>> Not sure if I understand your question. >>> >>> When constructing (pf | !p), 'pf' is kept and then !p could no longer >>> find the view it needs >>> in order to fetch the data. So the data needs to be fetched first: let >>> val x = !p in (pf | x) >>> >>> On Wed, Dec 12, 2018 at 10:19 AM Scott Murphy <[email protected]> >>> wrote: >>> >>>> 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]> >>>>> 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]. >>>>>> 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/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 >>>> >>>> <https://groups.google.com/d/msgid/ats-lang-users/3f188543-4655-42ca-8696-bb371641172f%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] <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/b6c63a79-458e-4e3a-b981-e2adbae17819%40googlegroups.com >> >> <https://groups.google.com/d/msgid/ats-lang-users/b6c63a79-458e-4e3a-b981-e2adbae17819%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/912401fc-52ff-4088-a5f2-6731c14be0e7%40googlegroups.com.
