BasicSpec.hascasl.output revision dc2ce67f56f9d4507503cc2a24f2646c7f2adf6d
1a38107941725211e7c3f051f7a8f5e12199f03acmaederclass Type < Type
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elknerclass TYPE < {x . x < t}
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillytype : Type- -> Type; Unit : TYPE
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillyclass a, b, c < Type
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescuclass a, b, c < Type; a < b
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillyprogram (pred tt : s) = \ (var x : s) . ()
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillyprogram __ res __ (x : s, y : t) : s = x;
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly fst (x : s, y : t) : s = x; snd (x : s, y : t) : t = y
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillypred eq : s * s
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyprogram all (p : (? s)) : (? Unit) = eq (p, tt)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyprogram And (x, y : (? Unit)) : (? Unit) = t1 () res t2 ()
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maederprogram __ impl __ (x, y : (? Unit)) = eq (x, x And y)
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maederprogram __ or __ (x, y : (? Unit)) : (? Unit) =
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder all (\ r : (? Unit) . ((x impl r) res (y impl r)) impl r);
e90dc723887d541f809007ae81c9bb73ced9592eChristian Maeder ex (p : (? s)) : (? Unit) =
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder all (\ r : (? Unit) . all (\ x : s . p (x) impl r) impl r);
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ff () : (? Unit) = all (\ r : (? Unit) . r ())
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'Reillyforall x : t; y : t
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder (fun __=__[t] : forall a : Type . a * a ->? Unit)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (var x : t, var y : t)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedertype Data1 ::= a |
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reillytype Data2 ::= Cons21 (Data1; Data2) |
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Cons22 (Data2; Data1) |
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillytype Data3 ::= Cons31 (sel1 :? Data1; sel2 :? Data2) |
c0833539c8cf577dd3f2497792fbdd818442744cChristian Maeder Cons32 (sel2 :? Data2; sel1 :? Data1)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillytype Data4 ::= Cons41 (sel1 :? Data1; sel2 :? Data2)? |
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Cons42 (sel2 :? Data2; sel1 :? Data1)?
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder. (fun true : Unit)
036ecbd8f721096321f47cf6a354a9d1bf3d032fChristian Maeder%% Classes ---------------------------------------------------------------
aa4d26536fffe0153cd81d28925985892ac2f300Christian MaederTYPE < {x . x < t}
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder%% Type Constructors -----------------------------------------------------
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder : Type < Data2
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly ::= a : Data1
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ::= Cons21 : Data1 * Data2 -> Data2 (Data1; Data2)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Cons22 : Data2 * Data1 -> Data2 (Data2; Data1)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder types Data1]%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ::= Cons31 : Data1 * Data2 -> Data3 (sel1 :? Data1; sel2 :? Data2)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Cons32 : Data2 * Data1 -> Data3 (sel2 :? Data2; sel1 :? Data1)]%
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder ::= Cons41 : Data1 * Data2 ->? Data4 (sel1 :? Data1; sel2 :? Data2)
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder Cons42 : Data2 * Data1 ->? Data4 (sel2 :? Data2; sel1 :? Data1)]%
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyPred : Type -> Type := \ a : Type . a ->? Unit
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyUnit : TYPE := Unit
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly__*__ : Type+ -> Type+ -> Type
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder__-->__ : Type- -> Type+ -> Type
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder__-->?__ : Type- -> Type+ -> Type
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder__->__ : Type- -> Type+ -> Type
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder__->?__ : Type- -> Type+ -> Type
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedert : Type %(var)%
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder%% Assumptions -----------------------------------------------------------
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyCons21 : Data1 * Data2 -> Data2 %(construct Data2)%
fa373bc327620e08861294716b4454be8d25669fChristian MaederCons22 : Data2 * Data1 -> Data2 %(construct Data2)%
fa373bc327620e08861294716b4454be8d25669fChristian MaederCons31 : Data1 * Data2 -> Data3 %(construct Data3)%
fa373bc327620e08861294716b4454be8d25669fChristian MaederCons32 : Data2 * Data1 -> Data3 %(construct Data3)%
fa373bc327620e08861294716b4454be8d25669fChristian MaederCons41 : Data1 * Data2 ->? Data4 %(construct Data4)%
fa373bc327620e08861294716b4454be8d25669fChristian MaederCons42 : Data2 * Data1 ->? Data4 %(construct Data4)%
fa373bc327620e08861294716b4454be8d25669fChristian Maeder__/\__ : Unit * Unit ->? Unit %(fun)%
fa373bc327620e08861294716b4454be8d25669fChristian Maeder__<=>__ : Unit * Unit ->? Unit %(fun)%
fa373bc327620e08861294716b4454be8d25669fChristian Maeder__=__ : forall a : Type . a * a ->? Unit %(fun)%
fa373bc327620e08861294716b4454be8d25669fChristian Maeder__=>__ : Unit * Unit ->? Unit %(fun)%
fa373bc327620e08861294716b4454be8d25669fChristian Maeder__=e=__ : forall a : Type . a * a ->? Unit %(fun)%
fa373bc327620e08861294716b4454be8d25669fChristian Maeder__\/__ : Unit * Unit ->? Unit %(fun)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder__if__ : Unit * Unit ->? Unit %(fun)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder__when__else__ : forall a : Type . a * Unit * a ->? a %(fun)%
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maedera : Data1 %(construct Data1)%
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'Reillyb : Data1 %(construct Data1)%
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maederbottom : forall a : Type . a %(fun)%
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maederc : Data1 %(construct Data1)%
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillydef__ : forall a : Type . a ->? Unit %(fun)%
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'Reillyeq : s * s ->? Unit %(pred)%
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian Maederfalse : Unit %(fun)%
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian Maedernot__ : Unit ->? Unit %(fun)%
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian Maeder : Data4 ->? Data1
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'Reilly %(select from Data4 constructed by
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Cons41 : Data1 * Data2 ->? Data4,
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Cons42 : Data2 * Data1 ->? Data4))%
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder : Data3 ->? Data1
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder %(select from Data3 constructed by
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Cons31 : Data1 * Data2 -> Data3,
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Cons32 : Data2 * Data1 -> Data3))%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder : Data4 ->? Data2
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder %(select from Data4 constructed by
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Cons41 : Data1 * Data2 ->? Data4,
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Cons42 : Data2 * Data1 ->? Data4))%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder : Data3 ->? Data2
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder %(select from Data3 constructed by
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Cons31 : Data1 * Data2 -> Data3,
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Cons32 : Data2 * Data1 -> Data3))%
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maedertrue : Unit %(fun)%
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maedertt : s ->? Unit %(op)%
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder%% Sentences -------------------------------------------------------------
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maederprogram (pred tt : s) = \ (var x : s) . () %(pe_tt)%
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder(fun __=__[t] : forall a : Type . a * a ->? Unit)
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder (var x : t, var y : t)
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder ::= a : Data1
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder c : Data1 %(ga_Data1)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ::= Cons21 : Data1 * Data2 -> Data2 (Data1; Data2)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Cons22 : Data2 * Data1 -> Data2 (Data2; Data1)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder types Data1 %(ga_Data2)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederforall x_1_1 : Data1; x_1_2 : Data2
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder . (fun __=__ : forall a : Type . a * a ->? Unit)
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder ((op sel1 : Data3 ->? Data1)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ((op Cons31 : Data1 * Data2 -> Data3)
ebd23ec61635b0bebf7969d14f65b9d1e39f2b26Liam O'Reilly (var x_1_1 : Data1, var x_1_2 : Data2)),
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder var x_1_1 : Data1) %(ga_select_sel1)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederforall x_1_1 : Data1; x_1_2 : Data2
ebd23ec61635b0bebf7969d14f65b9d1e39f2b26Liam O'Reilly . (fun __=__ : forall a : Type . a * a ->? Unit)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ((op sel2 : Data3 ->? Data2)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ((op Cons31 : Data1 * Data2 -> Data3)
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder (var x_1_1 : Data1, var x_1_2 : Data2)),
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder var x_1_2 : Data2) %(ga_select_sel2)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederforall x_1_1 : Data2; x_1_2 : Data1
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder . (fun __=__ : forall a : Type . a * a ->? Unit)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ((op sel2 : Data3 ->? Data2)
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder ((op Cons32 : Data2 * Data1 -> Data3)
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder (var x_1_1 : Data2, var x_1_2 : Data1)),
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder var x_1_1 : Data2) %(ga_select_sel2)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederforall x_1_1 : Data2; x_1_2 : Data1
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder . (fun __=__ : forall a : Type . a * a ->? Unit)
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder ((op sel1 : Data3 ->? Data1)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ((op Cons32 : Data2 * Data1 -> Data3)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (var x_1_1 : Data2, var x_1_2 : Data1)),
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder var x_1_2 : Data1) %(ga_select_sel1)%
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder ::= Cons31 : Data1 * Data2 -> Data3 (sel1 :? Data1; sel2 :? Data2)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder Cons32 : Data2 * Data1 -> Data3
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (sel2 :? Data2; sel1 :? Data1) %(ga_Data3)%
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederforall x_1_1 : Data1; x_1_2 : Data2
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder . (fun __=__ : forall a : Type . a * a ->? Unit)
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder ((op sel1 : Data4 ->? Data1)
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder ((op Cons41 : Data1 * Data2 ->? Data4)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder (var x_1_1 : Data1, var x_1_2 : Data2)),
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder var x_1_1 : Data1) %(ga_select_sel1)%
aa4d26536fffe0153cd81d28925985892ac2f300Christian Maederforall x_1_1 : Data1; x_1_2 : Data2
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder . (fun __=__ : forall a : Type . a * a ->? Unit)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ((op sel2 : Data4 ->? Data2)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ((op Cons41 : Data1 * Data2 ->? Data4)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (var x_1_1 : Data1, var x_1_2 : Data2)),
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder var x_1_2 : Data2) %(ga_select_sel2)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederforall x_1_1 : Data2; x_1_2 : Data1
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder . (fun __=__ : forall a : Type . a * a ->? Unit)
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder ((op sel2 : Data4 ->? Data2)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ((op Cons42 : Data2 * Data1 ->? Data4)
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly (var x_1_1 : Data2, var x_1_2 : Data1)),
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly var x_1_1 : Data2) %(ga_select_sel2)%
580f1724640a78be687e79d0ec95dd2665e77e91Liam O'Reillyforall x_1_1 : Data2; x_1_2 : Data1
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder . (fun __=__ : forall a : Type . a * a ->? Unit)
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder ((op sel1 : Data4 ->? Data1)
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder ((op Cons42 : Data2 * Data1 ->? Data4)
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder (var x_1_1 : Data2, var x_1_2 : Data1)),
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder var x_1_2 : Data1) %(ga_select_sel1)%
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reilly ::= Cons41 : Data1 * Data2 ->? Data4 (sel1 :? Data1; sel2 :? Data2)
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reilly Cons42 : Data2 * Data1 ->? Data4
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (sel2 :? Data2; sel1 :? Data1) %(ga_Data4)%
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder(fun true : Unit)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder%% Diagnostics -----------------------------------------------------------
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder*** Error 1.7, illegal universe class declaration 'Type'
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder*** Hint 3.5, is type variable 't'
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder*** FatalError 7.11, illegal type pattern argument: __
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder*** Error 11.16, undeclared class 'd'
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder*** Warning 11.7, redeclared class 'a'
d381ab99d6e2e56e09030577d65d9a118f246d35Christian Maeder*** Warning 11.10, redeclared class 'b'
d381ab99d6e2e56e09030577d65d9a118f246d35Christian Maeder*** Warning 11.13, redeclared class 'c'
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder*** Warning 11.19, redeclared class 'a'
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder*** Error 20.12, unexpected mixfix token: res
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder*** Hint 21.1, no type match for: fst
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder with type: '_var_3 ->? s' (21.20)
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly*** Hint 21.1, wrong result type 's' (21.20)
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly for application 'fst(var x : s, var y : t)'
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly*** Error 21.1, no typing for 'fst(var x : s, var y : t) : s'
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly*** Hint 22.1, no type match for: snd
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly with type: '_var_4 ->? t' (22.20)
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder*** Hint 22.1, wrong result type 't' (22.20)
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder for application 'snd(var x : s, var y : t)'
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder*** Error 22.1, no typing for 'snd(var x : s, var y : t) : t'
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder*** Hint 28.9, no type match for: all
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'Reilly with type: '_var_5 ->? ? Unit' (28.27)
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'Reilly*** Hint 28.9, wrong result type '? Unit' (28.27)
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'Reilly for application 'all(var p : ? s)'
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly*** Error 28.9, no typing for 'all(var p : ? s) : ? Unit'
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly*** Hint 30.9, no type match for: And
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly with type: '_var_7 ->? ? Unit' (30.32)
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly*** Hint 30.9, wrong result type '? Unit' (30.32)
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly for application 'And(var x : _var_6, var y : ? Unit)'
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly*** Error 30.9, no typing for 'And(var x : _var_6, var y : ? Unit) : ? Unit'
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly*** Error 32.12, unexpected mixfix token: impl
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly*** Error 34.12, unexpected mixfix token: or
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly*** Hint 37.3, no type match for: ex
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly with type: '_var_8 ->? ? Unit' (37.19)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder*** Hint 37.3, wrong result type '? Unit' (37.19)
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder for application 'ex(var p : ? s)'
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder*** Error 37.3, no typing for 'ex(var p : ? s) : ? Unit'
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder*** Hint 40.3, no type match for: ff
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder with type: '_var_9 ->? ? Unit' (40.12)
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder*** Hint 40.3, wrong result type '? Unit' (40.12)
45e2bc90dd11147156ddd7f9651ce8b2ec00f2a1Christian Maeder for application 'ff()'
45e2bc90dd11147156ddd7f9651ce8b2ec00f2a1Christian Maeder*** Error 40.3, no typing for 'ff() : ? Unit'
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder*** Error 66.25, unexpected mixfix token: e
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder*** Error 67.12, unexpected mixfix token: e