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
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).
>
Proofs are automatically eliminated after type-checking.
Proof construction offers an approach to internalizing constraint-solving.
For instance, with proofs, constraints involving multiplication can be
simplified
to only involve addition.
On Thu, Mar 8, 2018 at 9:59 PM, Brandon Barker
>> 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
