Yes, indeed, there are proof functions and proof values (as result of proof functions) ; the word “proof” used alone is typically to mean proof function (I was unclear).
Le samedi 23 mars 2019 22:35:51 UTC+1, gmhwxi a écrit : > > No, a proof is not a type. A proof is a total program (that is pure and > terminating). > > On Friday, March 22, 2019 at 1:55:17 PM UTC-4, Yannick Duchêne wrote: >> >> Within ATS, is it correct to say a proof is usually a dependant type? >> (whose value just get discarded from the generated program). >> >> >> P.S. Just wanted to have a quick look at some interesting talk here. >> Unfortunately, I still don’t have time to get back at ATS. >> > -- 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/b55b4963-eb49-48b1-8652-c6e208ccf848%40googlegroups.com.
