Anonymous user
Proof: Difference between revisions
note
(omit JavaScript) |
(note) |
||
Line 20:
Define a type of even numbers (0, 2, 4, 6, ...) within the previously defined range of natural numbers.
Prove that the addition of any two even numbers is even, if the result is a member of the type.
: '''''Note that this task only makes sense for [[wp:dependently-typed language|dependently-typed language]]s and [[wp:proof assistant|proof assistant]]s, or for languages with a type system strong enough to emulate certain dependent types. It does ''not'' ask you to implement a theorem prover yourself.'''''
=={{header|Agda}}==
| |||