2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maedervars a, b, c: Type
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maederops inl: a -> Sum a b;
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder inr: b -> Sum a b;
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder sumcase: (a ->? c) -> (b ->? c) -> Sum a b ->? c;
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maedervars f: a ->? c; g: b ->? c; h: Sum a b ->? c;
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder. h = sumcase f g <=>
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder forall x: a; y: b . h (inl x) = f x /\ h (inr y) = g y
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder. sumcase inl inr = \ z : Sum a b . z %implied
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maedervars x: a; y: b; z: Sum a b
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maederops outl: Sum a b -> a;
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder outr: Sum a b -> b
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder. outl = sumcase (\ x: a . x) (\ y: b . bot)
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder. outr = sumcase (\ x: a . bot) (\ y: b . y)
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maedertype Bool := Sum Unit Unit
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maedervars p: Bool; x,w: a
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maederops True, False: Bool;
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder if__then__else__ : Bool * a * a -> a
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder . True = inl ()
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder . False = inr ()
2083784cdbe448a3d8f94c7a0a0a011bbabf3fd0Christian Maeder . if p then x else w = sumcase (\ . x) (\ . w) p