type nat  = +{'zero : 1, 'succ : nat}
type even = +{'zero : 1, 'succ : odd}
type odd  = +{           'succ : even}

type nat_cover = (even * odd)  \/
                 (even * even) \/
                 (odd  * odd)  \/
                 (odd  * even)
comp ex1 : (nat * nat) -> <nat_cover>
   = fun x => <x>
eval z: <nat> = <'zero ()>
eval ex2 : <nat_cover> = let <x> = z in ex1 (x, x)

type nat_cover_no_oo = (even * odd)  \/
                       (even * even) \/
                       (odd  * even)
fail comp ex3 : (nat * nat) -> <nat_cover_no_oo>
   = fun x => <x>

Generated by Zeeshan Lakhani using scpaste at Sat Aug 10 01:37:13 2024. EDT. (original)