What is the `>>` operator?

[Yannick Duchêne]

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.

[Hongwei Xi]

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.

--
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.