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] > <javascript:>> 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] <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/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]. 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/b6c63a79-458e-4e3a-b981-e2adbae17819%40googlegroups.com.
