Proof: Difference between revisions
Commutativity of addition in OCaml
(OCaml version (now possible with GADT's)) |
(Commutativity of addition in OCaml) |
||
Line 689:
Exists_plus_even (Plus_succ (Plus_succ plus), Even_ss even)
(* 3.3 *)
</lang>▼
(* 0 + n = n *)
let rec plus_zero : type a. a nat -> (zero, a, a) plus = function
| Zero -> Plus_zero
| Succ a -> Plus_succ (plus_zero a)
(* a + b = n => (a + 1) + b = (n + 1) *)
let rec plus_succ_left : type a b sum. (a, b, sum) plus -> (a succ, b, sum succ) plus =
function
| Plus_zero -> Plus_zero
| Plus_succ plus -> Plus_succ (plus_succ_left plus)
(* a + b = n => b + a = n *)
let rec plus_commutative : type a b sum. a nat -> (a, b, sum) plus -> (b, a, sum) plus =
fun a plus ->
match plus with
| Plus_zero -> plus_zero a
| Plus_succ plus' ->
plus_succ_left (plus_commutative a plus')
▲</lang>
=={{header|Omega}}==
| |||