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

comp test1 : (nat - odd) -> <even>
   = fun x => <x>
comp test2 : (nat - even) -> <odd>
   = fun x => <x>
comp test3 : even -> <nat>
   = fun x => <x>
(* cannot be even and odd at the same time => bottom *)
comp test4 : (even /\ odd) -> <Bot>
   = fun x => <x>
comp test5 : even -> <nat - odd>
   = fun x => <x>
comp test6 : odd -> <nat - even>
   = fun x => <x>

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