annotate tests/case.ur @ 1272:56bd4a4f6e66

Some serious bug-fix work to get HTML example to compile; this includes fixing a bug with 'val' patterns in Unnest and the need for more local reduction in Especialize
author Adam Chlipala <adamc@hcoop.net>
date Thu, 03 Jun 2010 13:04:37 -0400
parents 71bafe66dbe1
children
rev   line source
adamc@170 1 datatype t = A | B
adamc@170 2
adamc@170 3 val swap = fn x : t => case x of A => B | B => A
adamc@170 4
adamc@170 5 datatype u = C of t | D
adamc@170 6
adamc@170 7 val out = fn x : u => case x of C y => y | D => A
adamc@170 8
adamc@170 9 datatype nat = O | S of nat
adamc@170 10
adamc@171 11 val is_two = fn x : nat =>
adamc@170 12 case x of S (S O) => A | _ => B
adamc@171 13
adamc@171 14 val zero_is_two = is_two O
adamc@171 15 val one_is_two = is_two (S O)
adamc@171 16 val two_is_two = is_two (S (S O))