The following article in the Effective-ATS series should be helpful: http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/PwTP-bool-vs-prop/index.html
On Thursday, March 8, 2018 at 9:54:13 PM UTC-5, gmhwxi wrote: > > > >> Aren't proofs a static construct ... > > No. This is a common misconception. Proofs are dynamic > but the evaluation of proofs cause no effect on the evaluation > of a program (containing proofs) and can thus be omitted. Often > this is referred to as proof irrelevance. > > You can think about it like this: > > Static terms are used to clarify dynamic terms. Proofs are clarified > by static terms (props) but they themselves cannot be used to clarify > dynamic terms. > > On Thu, Mar 8, 2018 at 9:47 PM, Brandon Barker <...> wrote: > >> I saw the following at the beginning of "A Tutorial on Programming >> Features in ATS": >> >> *The code in the dynamics of ATS is colored red unless it represents >> proofs, for which the color dark green is used* >> >> This is slightly confusing to me. (And I get the sense, maybe I asked >> this question before, years ago - if so, apologies): aren't proofs a static >> construct, in the sense that they aren't executed during a program's >> runtime? >> >> -- >> 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/29e80558-538d-4111-a4d8-aed95c83cb32%40googlegroups.com >> >> <https://groups.google.com/d/msgid/ats-lang-users/29e80558-538d-4111-a4d8-aed95c83cb32%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/47a2c4d4-6f93-4bc7-a306-0a1b806ffa4e%40googlegroups.com.
