vars a, b, c : Type

type Sum a b

ops inl : a -> Sum a b;

inr : b -> Sum a b;

sumcase : (a ->? c) -> (b ->? c) -> Sum a b ->? c;

bot : ? a

vars f : a ->? c; g : b ->? c; h : Sum a b ->? c

. h = sumcase f g

<=> forall x : a; y : b . h (inl x) = f x /\ h (inr y) = g y

. not def bot

. sumcase inl inr = \ z : Sum a b . z; %implied

vars x : a; y : b; z : Sum a b

ops outl : Sum a b -> a;

outr : Sum a b -> b

. outl = (sumcase \ x : a . x) \ y : b . bot

. outr = (sumcase \ x : a . bot) \ y : b . y;

type Bool := Sum Unit Unit

vars p : Bool; x, w : a

ops True, False : Bool;

if__then__else__ : Bool * a * a -> a

. True = inl ()

. False = inr ()

. if p then x else w = ((sumcase \ . x) \ . w) p;

types

Bool : Type;

Sum : Type -> Type -> Type

type

Bool := Sum Unit Unit

vars

a : Type %(var_1)%;

b : Type %(var_2)%;

c : Type %(var_3)%

op False : Bool

op True : Bool

op bot : forall a : Type . ? a

op if__then__else__ : forall a : Type . Bool * a * a -> a

op inl : forall a : Type; b : Type . a -> Sum a b

op inr : forall a : Type; b : Type . b -> Sum a b

op outl : forall a : Type; b : Type . Sum a b -> a

op outr : forall a : Type; b : Type . Sum a b -> b

op sumcase : forall a : Type; b : Type; c : Type

. (a ->? c) -> (b ->? c) -> Sum a b ->? c

vars

f : a ->? c;

g : b ->? c;

h : Sum a b ->? c;

p : Bool;

w : a;

x : a;

y : b;

z : Sum a b

forall

a : Type; b : Type; c : Type; f : a ->? c; g : b ->? c;

h : Sum a b ->? c

. h = sumcase f g

<=> forall x : a; y : b . h (inl x) = f x /\ h (inr y) = g y

. not def bot

forall a : Type; b : Type . sumcase inl inr = \ z : Sum a b . z

%implied

forall a : Type; b : Type

. outl = (sumcase \ x : a . x) \ y : b . bot

forall a : Type; b : Type

. outr = (sumcase \ x : a . bot) \ y : b . y

. True = inl ()

. False = inr ()

forall a : Type; p : Bool; w : a; x : a

. if p then x else w = ((sumcase \ . x) \ . w) p

1.6: ### Hint: is type variable 'a'

1.9: ### Hint: is type variable 'b'

1.12: ### Hint: is type variable 'c'

7.7: ### Hint: not a kind 'a ->? c'

7.19: ### Hint: not a kind 'b ->? c'

7.31: ### Hint: not a kind 'Sum a b ->? c'

9.11: ### Hint: not a class 'a'

9.17: ### Hint: not a class 'b'

10.3-10.5: *** Error:

in term 'not def (op bot : forall a : Type . ? a)'

are uninstantiated type variables

'[_v21_a]'

13.7: ### Hint: not a class 'a'

13.13: ### Hint: not a class 'b'

13.19: ### Hint: not a kind 'Sum a b'

16.21: ### Hint: rebound variable 'x'

16.34: ### Hint: rebound variable 'y'

17.21: ### Hint: rebound variable 'x'

17.36: ### Hint: rebound variable 'y'

20.7: ### Hint: not a class 'Bool'

20.16: ### Hint: not a class 'a'

20.15: ### Hint: rebound variable 'x'

20.18: ### Hint: not a class 'a'

22.25-22.28: ### Hint:

no kind found for 'Bool'

expected: {Cpo}

found: {Type}

22.25-22.28: ### Hint:

no kind found for 'Bool'

expected: {Cppo}

found: {Type}