On 07/30/2015 06:13 PM, Timon Gehr wrote:
...
The real difference is (roughly!) that the dependently typed interpreted
program always fails if it would fail in any possible execution


(This is ambiguous. What I mean is: If there is some execution in which it would fail.)

Reply via email to