>> 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 <brandon.bar...@gmail.com> 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 ats-lang-users+unsubscr...@googlegroups.com. > To post to this group, send email to ats-lang-users@googlegroups.com. > 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 ats-lang-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. 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/CAPPSPLr0DnPTrbc2%3Da0WiDTD1Y4xGJSgnRp6uctr_MfiDXGN6A%40mail.gmail.com.
