adamc@170: datatype t = A | B adamc@170: adamc@170: val swap = fn x : t => case x of A => B | B => A adamc@170: adamc@170: datatype u = C of t | D adamc@170: adamc@170: val out = fn x : u => case x of C y => y | D => A adamc@170: adamc@170: datatype nat = O | S of nat adamc@170: adamc@171: val is_two = fn x : nat => adamc@170: case x of S (S O) => A | _ => B adamc@171: adamc@171: val zero_is_two = is_two O adamc@171: val one_is_two = is_two (S O) adamc@171: val two_is_two = is_two (S (S O))