Prelude.hascasl.output revision 413db961f13e112716509b6d61d7a7bbf50c98b2
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder%% predefined universe containing all types,
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly%% superclass of all other classes
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillyclass Type < Type
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillyvar s : Type; t : Type
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu%% invisible type "Unit" for formulae
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly %% flat cpo with bottom
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly %% type aliases
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillypred true, false : Unit
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillypred __/\__, __\/__, __=>__, __if__, __<=>__ : Unit * Unit
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillypred not : Unit
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillypred __=__ : s * s
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly %% (builtin) type (constructors)
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maedertype __->?__ : -Type -> +Type -> Type
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder%% nested pairs are different from n-tupels (n > 2)
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maedertype __*__ : +Type -> +Type -> Type
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly%% "pred p args = e" abbreviates "op p args :? unit = e"
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'Reilly%% CASL requires "<=>" for pred-defn and disallows "()" as result
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maederop def, tt : Pred s
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyprogram (op def[s] : forall s : Type . Pred s) : Pred s =
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly \ (var x : s) . () : s ->? Unit
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly %% def is also total (identical to tt)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederprogram (op tt[s] : forall s : Type . Pred s) : Pred s =
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder \ (var x : s) . () : s ->? Unit
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder %% tt is total "op tt(x: s): unit = ()"
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reilly%% total function type
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedertype __->__ : -Type -> +Type -> Type
50c62c8c45643f09bcb2f4a99b07bf1d072ecf40Christian Maedertype __->__ < __->?__
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly%% total functions
c0833539c8cf577dd3f2497792fbdd818442744cChristian Maederop __res__ : forall s : Type; t : Type . s * t -> s
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly = \ ((var x : s), (var y : t)) .! (var x : s) as s
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyop fst : forall s : Type; t : Type . s * t -> s
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder = \ ((var x : s), (var y : t)) .! (var x : s) as s
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly%% trivial because its the strict function property
fa373bc327620e08861294716b4454be8d25669fChristian Maeder. (\ ((var x : s), (var y : t)) . def (x res y)) =
036ecbd8f721096321f47cf6a354a9d1bf3d032fChristian Maeder (\ ((var x : s), (var y : t)) . (def y) und (def x))
fa373bc327620e08861294716b4454be8d25669fChristian Maeder. (op fst[_v73; _v71] : forall s : Type; t : Type . s * t -> s) =
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder (op __res__[_v73; _v71] : forall s : Type; t : Type . s * t -> s)
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reilly%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly%% Internal Logic
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maederpred eq : s * s
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder. (\ (var x : s)
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly . (pred eq[s] : forall s : Type . s * s)
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly ((var x : s), (var x : s)))
53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly = (op tt[s] : forall s : Type . Pred s)
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly. (\ ((var x : s), (var y : s))
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly . (op __res__[s; Unit] : forall s : Type; t : Type . s * t -> s)
9e5f4073e948104307d43c3962d624b8416f191fLiam O'Reilly ((var x : s),
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (pred eq[s] : forall s : Type . s * s) ((var x : s), (var y : s))))
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (\ ((var x : s), (var y : s))
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder . (op __res__[s; Unit] : forall s : Type; t : Type . s * t -> s)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ((var y : s),
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (pred eq[s] : forall s : Type . s * s) ((var x : s), (var y : s))))
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder%% notation "\ ." abbreviates "\bla:unit."
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder%% where "bla" is never used, but only "()" instead
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder%% for type inference
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder%% an implicit cast from s to ?s of a term "e" yields the term "\ . e"
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder%% the cast from ?s to s is still done manually here (for the strict "und")
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder%% use "And" instead of "und" to avoid cast from "?unit" to "unit"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly%% the type instance for the first "eq" should be "?t"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly%% this is explicitely enforced by "\ .f(x)"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder%% Recursion (requires "free type nat ::= 0 | Suc(nat)" and "+"
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederclass Cpo < Type
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder {var c : Cpo;
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder pred __<<=__ : c * c;
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly pred isChain : forall c : Cpo . nat -> c
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly = \ (var s : nat -> c)
fa373bc327620e08861294716b4454be8d25669fChristian Maeder . all (\ n : nat . s (n) <<= s (Suc (n))) as Unit;
fa373bc327620e08861294716b4454be8d25669fChristian Maeder pred isBound : forall c : Cpo . c * (nat -> c)
fa373bc327620e08861294716b4454be8d25669fChristian Maeder = \ ((var x : c), (var s : nat -> c))
fa373bc327620e08861294716b4454be8d25669fChristian Maeder . all (\ n : nat . s (n) <<= x) as Unit;
fa373bc327620e08861294716b4454be8d25669fChristian Maeder op sup : (nat -> c) ->? c;}
fa373bc327620e08861294716b4454be8d25669fChristian Maederclass Pcpo < Cpo
fa373bc327620e08861294716b4454be8d25669fChristian Maeder {var p : Pcpo;
fa373bc327620e08861294716b4454be8d25669fChristian Maeder op bottom : p;}
fa373bc327620e08861294716b4454be8d25669fChristian Maederclass instance Flatcpo < Cpo
fa373bc327620e08861294716b4454be8d25669fChristian Maeder {var f : Flatcpo;}
fa373bc327620e08861294716b4454be8d25669fChristian Maedervar c : Cpo; d : Cpo
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedertype instance __*__ : +Cpo -> +Cpo -> Cpo
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedervar x1 : c; x2 : c; y1 : d; y2 : d
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maedertype instance __*__ : +Pcpo -> +Pcpo -> Pcpo
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'Reillytype Unit : Pcpo
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maedertype instance __-->?__ : -Cpo -> +Cpo -> Pcpo
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maedertype __-->?__ < __->?__
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'Reillytype instance __-->__ : -Cpo -> +Cpo -> Cpo
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian Maedervar f : c --> d; g : c --> d
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian Maedertype instance __-->__ : -Cpo -> +Pcpo -> Pcpo
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian Maederfun Y : (p --> p) --> p
e7cd36335f0f7be9ed5005e71d94c2856b588d62Christian Maedervar f : p --> p; x : p
e8d99f05c231b379be702a1aa8c7dd0b3c666928Liam O'Reilly. (var f : p --> p)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ((fun Y[p] : forall p : Pcpo . (p --> p) --> p) (var f : p --> p))
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder = (fun Y[p] : forall p : Pcpo . (p --> p) --> p) (var f : p --> p)
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder. (var f : p --> p) (var x : p) = (var x : p) =>
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (pred __<<=__[p] : forall c : Cpo . c * c)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ((fun Y[p] : forall p : Pcpo . (p --> p) --> p) (var f : p --> p),
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederop undefined : forall p : Pcpo; c : Cpo . c --> p
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder = (fun Y[c --> p] : forall p : Pcpo . (p --> p) --> p)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (\ (var x' : c --> p) . (var x' : c --> p) as
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (c --> p) --> c --> p)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederfree type bool ::= true |
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maedertype bool : Flatcpo
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maedertype nat : Flatcpo
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder%% Classes ---------------------------------------------------------------
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder%% Type Constructors -----------------------------------------------------
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder? : +Type -> Type
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian MaederLogical : Type := ? Unit
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian MaederPred : -Type -> Type := \ a : -Type . a ->? Unit
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederUnit : (Pcpo, Type)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder : (+Pcpo -> +Pcpo -> Pcpo, +Cpo -> +Cpo -> Cpo,
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder +Type -> +Type -> Type)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder__*__*__ : +Type -> +Type -> +Type -> Type
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder : (-Cpo -> +Pcpo -> Pcpo, -Cpo -> +Cpo -> Cpo,
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder -Type -> +Type -> Type) < (__-->?__, __->__)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder__-->?__ : (-Cpo -> +Cpo -> Pcpo, -Type -> +Type -> Type) < __->?__
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder__->__ : -Type -> +Type -> Type < __->?__
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder__->?__ : -Type -> +Type -> Type
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder : (Flatcpo, Type)
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder %[free type bool
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ::= true : bool
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder false : bool]%
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillynat : (Flatcpo, Type)
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder%% Type Variables --------------------------------------------------------
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederc : Cpo %(var_199)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederd : Cpo %(var_200)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederf : Flatcpo %(var_198)%
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maederp : Pcpo %(var_197)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedert : Type %(var_2)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder%% Assumptions -----------------------------------------------------------
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederY : forall p : Pcpo . (p --> p) --> p %(fun)%
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder__/\__ : Unit * Unit ->? Unit %(fun)%
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder__<<=__ : forall c : Cpo . c * c ->? Unit %(pred)%
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder__<=>__ : Unit * Unit ->? Unit %(fun)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder__=__ : forall s : Type . s * s ->? Unit %(fun)%
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder__=>__ : Unit * Unit ->? Unit %(fun)%
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder__=e=__ : forall a : Type . a * a ->? Unit %(fun)%
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder__\/__ : Unit * Unit ->? Unit %(fun)%
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder__if__ : Unit * Unit ->? Unit %(fun)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder : forall s : Type; t : Type . s * t -> s
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder %(op)% = \ ((var x : s), (var y : t)) .! (var x : s) as s
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederbottom : forall p : Pcpo . p %(fun)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederdef : forall s : Type . Pred s %(op)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maederdef__ : forall a : Type . a ->? Unit %(fun)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maedereq : forall s : Type . s * s ->? Unit %(pred)%
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder : bool %(construct bool)%
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder : Unit ->? Unit %(pred)%
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly : Unit %(fun)%
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly : forall s : Type; t : Type . s * t -> s
580f1724640a78be687e79d0ec95dd2665e77e91Liam O'Reilly %(op)% = \ ((var x : s), (var y : t)) .! (var x : s) as s
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder : forall c : Cpo . c * (nat -> c) ->? Unit
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder = \ ((var x : c), (var s : nat -> c))
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder . all (\ n : nat . s (n) <<= x) as Unit
f21c7417bdd1c0282025cba0f5cb0ff5bc5c98eeLiam O'Reilly : forall c : Cpo . (nat -> c) ->? Unit
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly = \ (var s : nat -> c)
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly . all (\ n : nat . s (n) <<= s (Suc (n))) as Unit
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reillynot : Unit ->? Unit %(pred)%
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reillynot__ : ? Unit ->? Unit %(fun)%
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maedersup : forall c : Cpo . (nat -> c) ->? c %(op)%
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly : bool %(construct bool)%
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder : Unit ->? Unit %(pred)%
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder : Unit %(fun)%
d381ab99d6e2e56e09030577d65d9a118f246d35Christian Maedertt : forall s : Type . Pred s %(op)%
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder : forall p : Pcpo; c : Cpo . c --> p
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder = (fun Y[c --> p] : forall p : Pcpo . (p --> p) --> p)
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder (\ (var x' : c --> p) . (var x' : c --> p) as
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder (c --> p) --> c --> p)
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly�__ : ? Unit ->? Unit %(fun)%
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly%% Variables -------------------------------------------------------------
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder%% Sentences -------------------------------------------------------------
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maederprogram def : Pred s = \ x . () : s ->? Unit
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'Reillyprogram tt : Pred s = \ x . () : s ->? Unit
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'Reillyforall x : s; y : t . x res y = (x as s)
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'Reillyforall x : s; y : t . fst (x, y) = (x as s)
7d96b1ef2b8597330aedee6713615ec15508edcfLiam O'Reilly(\ (x, y) . def (x res y)) = (\ (x, y) . (def y) und (def x))
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly(\ x . eq (x, x)) = tt
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly(\ (x, y) . x res eq (x, y)) = (\ (x, y) . y res eq (x, y))
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reillyforall s : nat -> c
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly . isChain s = (all (\ n : nat . s (n) <<= s (Suc (n))) as Unit)
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reillyforall x : c; s : nat -> c
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly . isBound (x, s) = (all (\ n : nat . s (n) <<= x) as Unit)
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reillyf x = x => Y f <<= x
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reillyundefined = (Y (\ x' . x' as (c --> p) --> c --> p) as c --> p)
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reillyfree type bool
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly ::= true : bool
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder%% Diagnostics -----------------------------------------------------------
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly*** Warning 4.7, void universe class declaration 'Type'
bc350328e6ac2d9074317e222b4207a6aa49afeaLiam O'Reilly*** Hint 6.5, is type variable 's'
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder*** Hint 6.7, is type variable 't'
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder*** Hint 11.6, redeclared type 'Unit'
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder*** Error 14.11, illegal type pattern argument '__'
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder*** Error 15.8, illegal type pattern argument '__'
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder*** Warning 17.6, ignoring declaration for builtin identifier 'true'
dc403ff45531bc75a7544b8b5fc52a5217a1a54aChristian Maeder*** Warning 17.12, ignoring declaration for builtin identifier 'false'
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder*** Warning 19.9, ignoring declaration for builtin identifier '__/\__'
45e2bc90dd11147156ddd7f9651ce8b2ec00f2a1Christian Maeder*** Warning 19.17, ignoring declaration for builtin identifier '__\/__'
45e2bc90dd11147156ddd7f9651ce8b2ec00f2a1Christian Maeder*** Warning 19.25, ignoring declaration for builtin identifier '__=>__'
ee48a7a67da604356b665e51aa7545536a09b737Christian Maeder*** Warning 19.33, ignoring declaration for builtin identifier '__if__'
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder*** Warning 19.40, ignoring declaration for builtin identifier '__<=>__'
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder*** Warning 22.8, ignoring declaration for builtin identifier '__=__'
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder*** Hint 27.8, redeclared type '__->?__'
f19dc06364e8d6ea36f7c170e1f7a0677de63184Liam O'Reilly*** Hint 30.8, redeclared type '__*__'
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Error 31.6-31.12, illegal type pattern '__ * __ * __'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Hint 40.7, not a class 's'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Hint 42.16, rebound variable 'x'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Hint 44.15, rebound variable 'x'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Error 46.11, unexpected mixfix token: und
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Hint 50.8, redeclared type '__->__'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Hint 52.8, redeclared type '__->__'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Hint, repeated supertype '__->?__'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Error 54.42-54.49, ambiguous mixfix term
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Error 54.32, unexpected mixfix token: all
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Error 54.6, unexpected mixfix token: :
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Hint 58.13, rebound variable 'x'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Hint 59.9, rebound variable 'x'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Hint 60.9, no type match for: snd
b1f12c962a6fb28a298b36cf6a1dcf2ad788fb58Christian Maeder with (maximal) type: _v11 ->? t
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Hint 60.9-60.24, untypable application (with result type: t)
fa373bc327620e08861294716b4454be8d25669fChristian Maeder 'snd (x : s, (var y : t))'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Error 60.30, no typing for 'program snd (x : s, (var y : t)) : t = y'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Error 65.18-65.30, ambiguous mixfix term
fa373bc327620e08861294716b4454be8d25669fChristian Maeder def (__res__(x, y))
fa373bc327620e08861294716b4454be8d25669fChristian Maeder def__(__res__(x, y))
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Error 65.59, unexpected mixfix token: und
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Hint 65.7, rebound variable 'x'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Error 65.18-65.30, unexpected term 'def (x res y)'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Hint 65.40, rebound variable 'x'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Error 65.51-65.69, unexpected term '(def y) und (def x)'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Hint 74.5, rebound variable 'x'
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Hint 75.6, rebound variable 'x'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Hint 75.35, rebound variable 'x'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Warning 85.6, new type shadows type variable 's'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Error 85.11, illegal type variable as supertype 's'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Hint 87.9, no type match for: all
fa373bc327620e08861294716b4454be8d25669fChristian Maeder with (maximal) type: _v187 ->? Pred Unit
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Hint 87.9-87.15, untypable application (with result type: Pred Unit)
fa373bc327620e08861294716b4454be8d25669fChristian Maeder 'all (var p : Pred s)'
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Error 87.38, no typing for 'program all (var p : Pred s) : Pred Unit = eq (p, tt)'
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Error 90.45, unexpected mixfix token: t1
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Error 93.11, unexpected mixfix token: impl
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Error 93.58, unexpected mixfix token: And
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Error 95.11, unexpected mixfix token: or
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Error 96.21, unexpected mixfix token: impl
fa373bc327620e08861294716b4454be8d25669fChristian Maeder*** Error 95.48, unexpected mixfix token: all
56899f6457976a2ee20f6a23f088cb5655b15715Liam O'Reilly*** Error 99.32, unexpected mixfix token: impl
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Error 99.17, unexpected mixfix token: all
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Error 98.39, unexpected mixfix token: all
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Error 101.29, unexpected mixfix token: all
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Error 103.44, unexpected mixfix token: impl
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Error 108.51, unexpected mixfix token: impl
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Error 108.22, unexpected mixfix token: all
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Error 108.3, unexpected mixfix token: all
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Hint 117.5, is type variable 'c'
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Error 121.3, unexpected mixfix token: all
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Error 122.31, unexpected mixfix token: und
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Error 122.3, unexpected mixfix token: all
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Error 123.31, unexpected mixfix token: und
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Error 123.3, unexpected mixfix token: all
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Error 125.55, unexpected mixfix token: Suc
eb48217dfa67ddb87b8fbd846de293d0636bd578Christian Maeder*** Error 125.32, unexpected mixfix token: all
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Error 125.32-125.62, unexpected term 'all (\ n : nat . s (n) <<= s (Suc (n)))'
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Hint 126.15, rebound variable 'x'
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Error 126.38, unexpected mixfix token: all
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Error 126.38-126.60, unexpected term 'all (\ n : nat . s (n) <<= x)'
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Error 131.56, unexpected mixfix token: impl
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly*** Error 130.32, unexpected mixfix token: impl
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder*** Error 130.3, unexpected mixfix token: all
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder*** Error 134.31, unexpected mixfix token: impl
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder*** Error 134.3, unexpected mixfix token: all
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder*** Hint 139.5, is type variable 'p'
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder*** Warning 141.4, ignoring declaration for builtin identifier 'bottom'
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder*** Error 143.3, unexpected mixfix token: all
66bc8d6e69cde43f1ccbeb76104cf7b8038acd6cChristian Maeder*** Hint 148.6, is type variable 'f'
ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian Maeder*** Error 150.15, unexpected mixfix token: [
ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian Maeder*** Hint 153.5, is type variable 'c'
ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian Maeder*** Hint 153.5, rebound type variable 'c'
ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian Maeder*** Hint 153.8, is type variable 'd'
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Hint 157.7, not a class 'c'
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Hint 157.11, not a class 'c'
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Hint 157.18, not a class 'd'
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Hint 157.23, not a class 'd'
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Error 159.45, unexpected mixfix token: und
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly*** Hint 169.9, redeclared type '__-->?__'
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly*** Hint, repeated supertype '__->?__'
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly*** Error 171.35, unexpected mixfix token: und
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly*** Error 174.45, unexpected mixfix token: +
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly*** Error 173.40, unexpected mixfix token: und
648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder*** Error 172.39, unexpected mixfix token: und
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder*** Error 171.9, unexpected mixfix token: all
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder*** Error 170.7, unexpected mixfix token: :
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Error 176.51, unexpected mixfix token: impl
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Error 176.31, unexpected mixfix token: all
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder*** Error 181.9, non-unique kind for '__-->__'
d381ab99d6e2e56e09030577d65d9a118f246d35Christian Maeder*** Error 182.46-182.53, ambiguous mixfix term
580f1724640a78be687e79d0ec95dd2665e77e91Liam O'Reilly*** Error 182.36, unexpected mixfix token: all
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly*** Error 182.7, unexpected mixfix token: :
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder*** Hint 184.7, not a kind 'c --> d'
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder*** Hint 184.11, not a kind 'c --> d'
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder*** Error 186.26, unexpected mixfix token: c
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Error 193.32, unexpected mixfix token: impl
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Error 192.40, unexpected mixfix token: und
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder*** Error 192.3, unexpected mixfix token: all
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Hint 195.7, not a kind 'p --> p'
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder*** Hint 195.5, rebound variable 'f'
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder*** Hint 195.20, not a class 'p'
a00461fcf7432205a79a0f12dbe6c1ebc58bc000Christian Maeder*** Hint 195.18, rebound variable 'x'
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Warning 204.20, ignoring declaration for builtin identifier 'true'
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder*** Warning 204.27, ignoring declaration for builtin identifier 'false'