Re:Announcing Rust 1.20
by catnaroek on Friday September 01, 2017 @06:24PM
(#15152820)
> defined(a,i,j) and defined(a[j+1]) implies defined(a,i,j+1) is a theorem. (proof)
Sure. My point is just that a theorem is a proposition equipped with a proof. If the user just enters a proposition into the system, then they aren't entering a theorem. They're entering a proposition that the system can turn into a theorem.
Sure. My point is just that a theorem is a proposition equipped with a proof. If the user just enters a proposition into the system, then they aren't entering a theorem. They're entering a proposition that the system can turn into a theorem.