3 ms·
I don't see the problem here. I said that Idris will reject the program if the proof fails. That's what you're saying too, unless I'm very confused. (It's late,
by gary_bernhardt 10y ago
I don't see the problem here. I said that Idris will reject the program if the proof fails. That's what you're saying too, unless I'm very confused. (It's late, so maybe I am?)
- arianvanp 10y agoYes, but it might also reject correct programs. that's the point I'm trying to make.
- gary_bernhardt 10y agoThat doesn't contradict the quote that you provided. The quote just says "the compiler will reject the program at compile time [if there's no valid proof]", which is true.