Do the >> operator as in p1 >> p2 means the proof p1 is changed into
the proof p2 in place?
It’s not really explained in the docs, except here:
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/c3302.html
.
Then a function call f(…, pf, …) on some proof variable
pf of the view V1 is to change the view of pf into V2 upon
its return. In the case where V1 and V2 are the same,
!V1 >> V2 can simply be written as !V1.
The interpretation I make of it is uncertain to me.
If it’s really as I guess, that is it change a proof into another in place,
then why not returning a new proof instead? May be the reason is the key to
understand this operator.
Yes, your guess is correct.
then why not returning a new proof instead
This is called proof threading. Returning a new proof is fine in theory,
but it does make coding a lot more verbose.On Thu, May 21, 2015 at 6:13 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:
Do the >> operator as in p1 >> p2 means the proof p1 is changed into
the proof p2 in place?
It’s not really explained in the docs, except here:
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/c3302.html
.
Then a function call f(…, pf, …) on some proof variable
pf of the view V1 is to change the view of pf into V2 upon
its return. In the case where V1 and V2 are the same,
!V1 >> V2 can simply be written as !V1.
The interpretation I make of it is uncertain to me.
If it’s really as I guess, that is it change a proof into another in
place, then why not returning a new proof instead? May be the reason is the
key to understand this operator.
–
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/9298389e-f4e8-48fe-a093-c09aeb1f46c2%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/9298389e-f4e8-48fe-a093-c09aeb1f46c2%40googlegroups.com?utm_medium=email&utm_source=footer
.