Coproducts.hascasl.output revision f55c7ffbcd378316d8547132be02b10c5eb4dfb2
b7ff1e47da4653d2ff1ec7b489e6067fed29d8c5Lennart Poetteringvars a, b, c : Type
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poetteringops inl : a -> Sum a b;
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poettering inr : b -> Sum a b;
b7ff1e47da4653d2ff1ec7b489e6067fed29d8c5Lennart Poettering sumcase : (a ->? c) -> (b ->? c) -> Sum a b ->? c;
c32e0c40f7e706e3ebcd101187d5ced96f083491Lennart Poetteringvars f : a ->? c; g : b ->? c; h : Sum a b ->? c
c32e0c40f7e706e3ebcd101187d5ced96f083491Lennart Poettering. h = sumcase f g
7d640cdf66a7c032c871ccfe0ee4ad56f7e3869bLennart Poettering <=> forall x : a; y : b . h (inl x) = f x /\ h (inr y) = g y
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poettering. sumcase inl inr = \ z : Sum a b . z; %implied
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poetteringvars x : a; y : b; z : Sum a b
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poetteringops outl : Sum a b -> a;
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poettering outr : Sum a b -> b
7d640cdf66a7c032c871ccfe0ee4ad56f7e3869bLennart Poettering. outl = (sumcase \ x : a . x) \ y : b . bot
6e25b33cddf77c90d351dee6442c51bd19e2b7a8Lennart Poettering. outr = (sumcase \ x : a . bot) \ y : b . y;
34df5a34e1d0ac4bba453fb5f52f18a2f5f260f9Lennart Poetteringtype Bool := Sum Unit Unit
34df5a34e1d0ac4bba453fb5f52f18a2f5f260f9Lennart Poetteringvars p : Bool; x, w : a
7d640cdf66a7c032c871ccfe0ee4ad56f7e3869bLennart Poetteringops True, False : Bool;
34df5a34e1d0ac4bba453fb5f52f18a2f5f260f9Lennart Poettering if__then__else__ : Bool * a * a -> a
099663ff8c117303af369a4d412dafed0c5614c2Lennart Poettering. True = inl ()
099663ff8c117303af369a4d412dafed0c5614c2Lennart Poettering. False = inr ()
099663ff8c117303af369a4d412dafed0c5614c2Lennart Poettering. if p then x else w = ((sumcase \ . x) \ . w) p;
a0e155d440173ba524918cb3800350b452952082Lennart PoetteringSum : Type -> Type -> Type
9700edb4e836f95815ee3237e5bc8d224b5014d7Lennart PoetteringBool : Type := Sum Unit Unit
f1dd0c3f9b4a257e81ff9c6a08070c702a0db45aLennart Poetteringa : Type %(var_1)%;
f1dd0c3f9b4a257e81ff9c6a08070c702a0db45aLennart Poetteringb : Type %(var_2)%;
fc7ac59412742e2ef0638e86070c33afd579848eLennart Poetteringc : Type %(var_3)%
260abb780a135e4cae8c10715c7e85675efc345aLennart Poetteringop False : Bool %(op)%
260abb780a135e4cae8c10715c7e85675efc345aLennart Poetteringop True : Bool %(op)%
260abb780a135e4cae8c10715c7e85675efc345aLennart Poetteringop bot : forall a : Type . ? a %(op)%
4d99d2fd3cc3c02173ad935f94a6f96195fc9e2bKay Sieversop if__then__else__ : forall a : Type . Bool * a * a -> a %(op)%
4d99d2fd3cc3c02173ad935f94a6f96195fc9e2bKay Sieversop inl : forall a : Type; b : Type . a -> Sum a b %(op)%
4d99d2fd3cc3c02173ad935f94a6f96195fc9e2bKay Sieversop inr : forall a : Type; b : Type . b -> Sum a b %(op)%
260abb780a135e4cae8c10715c7e85675efc345aLennart Poetteringop outl : forall a : Type; b : Type . Sum a b -> a %(op)%
260abb780a135e4cae8c10715c7e85675efc345aLennart Poetteringop outr : forall a : Type; b : Type . Sum a b -> b %(op)%
260abb780a135e4cae8c10715c7e85675efc345aLennart Poetteringop sumcase : forall a : Type; b : Type; c : Type
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering . (a ->? c) -> (b ->? c) -> Sum a b ->? c
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sieversh : Sum a b ->? c;
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sieversa : Type; b : Type; c : Type; f : a ->? c; g : b ->? c;
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sieversh : Sum a b ->? c
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers. h = sumcase f g
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers <=> forall x : a; y : b . h (inl x) = f x /\ h (inr y) = g y
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers. not def bot
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sieversforall a : Type; b : Type . sumcase inl inr = \ z : Sum a b . z
2791a8f8dc8764a9247cdba3562bd4c04010f144Lennart Poetteringforall a : Type; b : Type
a49408ec64063023524b964064d393c1fce36e4aKay Sievers. outl = (sumcase \ x : a . x) \ y : b . bot
a49408ec64063023524b964064d393c1fce36e4aKay Sieversforall a : Type; b : Type
a49408ec64063023524b964064d393c1fce36e4aKay Sievers. outr = (sumcase \ x : a . bot) \ y : b . y
a49408ec64063023524b964064d393c1fce36e4aKay Sievers. True = inl ()
099663ff8c117303af369a4d412dafed0c5614c2Lennart Poettering. False = inr ()
099663ff8c117303af369a4d412dafed0c5614c2Lennart Poetteringforall a : Type; p : Bool; w : a; x : a
a8f11321c209830a35edd0357e8def5d4437d854Lennart Poettering. if p then x else w = ((sumcase \ . x) \ . w) p
a8f11321c209830a35edd0357e8def5d4437d854Lennart Poettering### Hint 1.6, is type variable 'a'
81253930180bac6b6fb372a9c7bea724bd795c86Lennart Poettering### Hint 1.9, is type variable 'b'
81253930180bac6b6fb372a9c7bea724bd795c86Lennart Poettering### Hint 1.12, is type variable 'c'
81253930180bac6b6fb372a9c7bea724bd795c86Lennart Poettering### Hint 7.7, not a kind 'a ->? c'
7fc7012b8b54bdd6610d32649d4ee9c938a4843dLennart Poettering### Hint 7.19, not a kind 'b ->? c'
430c18ed7f576fd9041b0a02e7c4210bdd020a25Lennart Poettering### Hint 7.31, not a kind 'Sum a b ->? c'
1a6f4df6c9437ed631080b7e006f666326063d36Lennart Poettering### Hint 9.11, not a class 'a'
1a6f4df6c9437ed631080b7e006f666326063d36Lennart Poettering### Hint 9.17, not a class 'b'
1a6f4df6c9437ed631080b7e006f666326063d36Lennart Poettering*** Error 10.3, in term 'not def (op bot : forall a : Type . ? a)[_v92_a]'
a49408ec64063023524b964064d393c1fce36e4aKay Sievers are uninstantiated type variables '[_v92_a]'
3db48a7850d9ceb8e81ec4ad410520c05c008763Lennart Poettering### Hint 13.7, not a class 'a'
3db48a7850d9ceb8e81ec4ad410520c05c008763Lennart Poettering### Hint 13.13, not a class 'b'
a49408ec64063023524b964064d393c1fce36e4aKay Sievers### Hint 13.19, not a kind 'Sum a b'
a49408ec64063023524b964064d393c1fce36e4aKay Sievers### Hint 16.21, rebound variable 'x'
3db48a7850d9ceb8e81ec4ad410520c05c008763Lennart Poettering### Hint 16.34, rebound variable 'y'
2e0d98fa87a4e399763c8235abe56be4f8ac7fb8Lennart Poettering### Hint 17.21, rebound variable 'x'
2e0d98fa87a4e399763c8235abe56be4f8ac7fb8Lennart Poettering### Hint 17.36, rebound variable 'y'
62170515a17d0771aa38c8e7711a7a60c8d14d2fLennart Poettering### Hint 20.7, not a class 'Bool'
a49408ec64063023524b964064d393c1fce36e4aKay Sievers### Hint 20.16, not a class 'a'
62170515a17d0771aa38c8e7711a7a60c8d14d2fLennart Poettering### Hint 20.15, rebound variable 'x'
b5c6cf87342bedeb67fbbc4f3f512af1603a461cLennart Poettering### Hint 20.18, not a class 'a'