Prelude.hascasl.output revision 81946e2b3f6dde6167f48769bd02c7a634736856
%% predefined universe containing all types,
%% superclass of all other classes
class Type < Type
var s : Type; t : Type
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% invisible type "Unit" for formulae
type Unit
%% flat cpo with bottom
%% type aliases
pred true, false : Unit
pred __/\__, __\/__, __=>__, __if__, __<=>__ : Unit * Unit
pred not : Unit
pred __=__ : s * s
%% =e=
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% (builtin) type (constructors)
type __->?__ : -Type -> +Type -> Type
%% nested pairs are different from n-tupels (n > 2)
type __*__ : +Type -> +Type -> Type
%% ...
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% "pred p args = e" abbreviates "op p args :? unit = e"
%% CASL requires "<=>" for pred-defn and disallows "()" as result
op def, tt : Pred s
var x : s
program (op def[s]
: forall s : Type . Pred s_v-1@(s_v-1 ->? Unit)) :
Pred s@(s ->? Unit)
= (\ (var x : s) : s . ()) : s ->? Unit
%% def is also total (identical to tt)
program (op tt[s]
: forall s : Type . Pred s_v-1@(s_v-1 ->? Unit)) :
Pred s@(s ->? Unit)
= (\ (var x : s) : s . ()) : s ->? Unit
%% tt is total "op tt(x: s): unit = ()"
%% total function type
type __->__ : -Type -> +Type -> Type
type __->__ < __->?__
%% total functions
op __res__ : forall s : Type; t : Type . s_v-1 * t_v-2 -> s_v-1
= \ (var x : s, var y : t) .! (var x : s) as s_v1
op fst : forall s : Type; t : Type . s_v-1 * t_v-2 -> s_v-1
= \ (var x : s, var y : t) .! (var x : s) as s_v1
%% trivial because its the strict function property
. ((fun __=__[((s * _var_37_v37) ->? _var_33_v33)]
: forall s : Type . s_v-1 * s_v-1 ->? Unit) :
((s * _var_37_v37) ->? _var_33_v33) *
((s * _var_37_v37) ->? _var_33_v33) ->? Unit)
((\ ((var x : s) : s, var y : _var_37_v37) . def (x res y)) :
(s * _var_37_v37) ->? _var_33_v33,
(\ ((var x : s) : s, var y : _var_37_v37) . (def y) und (def x)) :
(s * _var_37_v37) ->? _var_33_v33) :
Unit
. ((fun __=__[((_var_73_v73 * _var_71_v71) -> _var_73_v73)]
: forall s : Type . s_v-1 * s_v-1 ->? Unit) :
((_var_73_v73 * _var_71_v71) -> _var_73_v73) *
((_var_73_v73 * _var_71_v71) -> _var_73_v73) ->? Unit)
((op fst[_var_73_v73; _var_71_v71]
: forall s : Type; t : Type . s_v-1 * t_v-2 -> s_v-1) :
_var_73_v73 * _var_71_v71 -> _var_73_v73,
(op __res__[_var_73_v73; _var_71_v71]
: forall s : Type; t : Type . s_v-1 * t_v-2 -> s_v-1) :
_var_73_v73 * _var_71_v71 -> _var_73_v73) :
Unit
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Internal Logic
pred eq : s * s
. ((fun __=__[(s ->? Unit)]
: forall s : Type . s_v-1 * s_v-1 ->? Unit) :
(s ->? Unit) * (s ->? Unit) ->? Unit)
((\ (var x : s) : s
. ((pred eq[s] : forall s : Type . s_v-1 * s_v-1) : s * s ->? Unit)
(var x : s, var x : s) :
Unit) :
s ->? Unit,
(op tt[s] : forall s : Type . Pred s_v-1@(s_v-1 ->? Unit)) :
Pred s@(s ->? Unit)) :
Unit
. ((fun __=__[((s * s) ->? s)]
: forall s : Type . s_v-1 * s_v-1 ->? Unit) :
((s * s) ->? s) * ((s * s) ->? s) ->? Unit)
((\ (var x : s, var y : s)
. ((op __res__[s; Unit]
: forall s : Type; t : Type . s_v-1 * t_v-2 -> s_v-1) :
s * Unit -> s)
(var x : s,
((pred eq[s] : forall s : Type . s_v-1 * s_v-1) : s * s ->? Unit)
(var x : s, var y : s) :
Unit) :
s) :
(s * s) ->? s,
(\ (var x : s, var y : s)
. ((op __res__[s; Unit]
: forall s : Type; t : Type . s_v-1 * t_v-2 -> s_v-1) :
s * Unit -> s)
(var y : s,
((pred eq[s] : forall s : Type . s_v-1 * s_v-1) : s * s ->? Unit)
(var x : s, var y : s) :
Unit) :
s) :
(s * s) ->? s) :
Unit
%% then %def
%% notation "\ ." abbreviates "\bla:unit."
%% where "bla" is never used, but only "()" instead
%% for type inference
%% an implicit cast from s to ?s of a term "e" yields the term "\ . e"
type s < ? s_v1
%% the cast from ?s to s is still done manually here (for the strict "und")
%% use "And" instead of "und" to avoid cast from "?unit" to "unit"
%% the type instance for the first "eq" should be "?t"
%% this is explicitely enforced by "\ .f(x)"
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Recursion (requires "free type nat ::= 0 | Suc(nat)" and "+"
type nat
class Cpo < Type
{var c : Cpo; pred __<<=__ : c * c; ;
pred isChain : forall c : Cpo . nat -> c_v-1
= \ (var s : nat -> c)
. (all (\ n : nat . s (n) <<= s (Suc (n)))) as Unit;
pred isBound : forall c : Cpo . c_v-1 * (nat -> c_v-1)
= \ (var x : c, var s : nat -> c)
. (all (\ n : nat . s (n) <<= x)) as Unit;
op sup : (nat -> c) ->? c;}
class Pcpo < Cpo
{var p : Pcpo; op bottom : p;}
class instance Flatcpo < Cpo
{var f : Flatcpo;}
var c : Cpo; d : Cpo
type instance __*__ : +Cpo -> +Cpo -> Cpo
var x1 : c; x2 : c; y1 : d; y2 : d
type instance __*__ : +Pcpo -> +Pcpo -> Pcpo
type Unit : Pcpo
%% Pcont
type instance __-->?__ : -Cpo -> +Cpo -> Pcpo
type __-->?__ < __->?__
%% Tcont
type instance __-->__ : -Cpo -> +Cpo -> Cpo
var f : c --> d; g : c --> d
type instance __-->__ : -Cpo -> +Pcpo -> Pcpo
fun Y : (p --> p) --> p
var f : p --> p; x : p
. ((fun __=__[p] : forall s : Type . s_v-1 * s_v-1 ->? Unit) :
p * p ->? Unit)
((var f : p --> p)
(((fun Y[p] : forall p : Pcpo . (p_v-1 --> p_v-1) --> p_v-1) :
(p --> p) --> p)
(var f : p --> p) :
p) :
p,
((fun Y[p] : forall p : Pcpo . (p_v-1 --> p_v-1) --> p_v-1) :
(p --> p) --> p)
(var f : p --> p) :
p) :
Unit
. (fun __=>__ : Unit * Unit ->? Unit)
(((fun __=__[p] : forall s : Type . s_v-1 * s_v-1 ->? Unit) :
p * p ->? Unit)
((var f : p --> p)(var x : p) : p, var x : p) :
Unit,
((pred __<<=__[p] : forall c : Cpo . c_v-1 * c_v-1) :
p * p ->? Unit)
(((fun Y[p] : forall p : Pcpo . (p_v-1 --> p_v-1) --> p_v-1) :
(p --> p) --> p)
(var f : p --> p) :
p,
var x : p) :
Unit) :
Unit
op undefined : forall p : Pcpo; c : Cpo . c_v-2 --> p_v-1
= (((fun Y[(c --> p)]
: forall p : Pcpo . (p_v-1 --> p_v-1) --> p_v-1) :
((c --> p) --> (c --> p)) --> (c --> p))
(((\ (var x' : _var_284_v284 --> p_v197)
. (var x' : _var_284_v284 --> p_v197)) :
(_var_284_v284 --> p) ->? (_var_284_v284 --> p)) as
(c --> p) --> c --> p) :
(c --> p)) as
_var_284_v284 --> p_v197
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% user stuff
free type bool ::= true |
false
type bool : Flatcpo
type nat : Flatcpo
%% Classes ---------------------------------------------------------------
Cpo < Type
Flatcpo < Cpo
Pcpo < Cpo
%% Type Constructors -----------------------------------------------------
Logical : Type := Unit ->? Unit
Pred : -Type -> Type := \ a : -Type . a_v-1 ->? Unit
Unit : (Pcpo, Type)
__*__
: (+Pcpo -> +Pcpo -> Pcpo, +Cpo -> +Cpo -> Cpo,
+Type -> +Type -> Type)
__*__*__ : +Type -> +Type -> +Type -> Type
__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type
__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type
__-->__
: (-Cpo -> +Pcpo -> Pcpo, -Cpo -> +Cpo -> Cpo,
-Type -> +Type -> Type) < (__-->?__, __->__)
__-->?__ : (-Cpo -> +Cpo -> Pcpo, -Type -> +Type -> Type) < __->?__
__->__ : -Type -> +Type -> Type < __->?__
__->?__ : -Type -> +Type -> Type
bool
: (Flatcpo, Type)
%[free type bool
::= true : bool
false : bool]%
nat : (Flatcpo, Type)
s : Type < ? s_v1
%% Type Variables --------------------------------------------------------
c : Cpo %(var_199)%
d : Cpo %(var_200)%
f : Flatcpo %(var_198)%
p : Pcpo %(var_197)%
t : Type %(var_2)%
%% Assumptions -----------------------------------------------------------
Y : forall p : Pcpo . (p_v-1 --> p_v-1) --> p_v-1 %(fun)%
__/\__ : Unit * Unit ->? Unit %(fun)%
__<<=__ : forall c : Cpo . c_v-1 * c_v-1 ->? Unit %(pred)%
__<=>__ : Unit * Unit ->? Unit %(fun)%
__=__ : forall s : Type . s_v-1 * s_v-1 ->? Unit %(fun)%
__=>__ : Unit * Unit ->? Unit %(fun)%
__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__\/__ : Unit * Unit ->? Unit %(fun)%
__if__ : Unit * Unit ->? Unit %(fun)%
__res__
: forall s : Type; t : Type . s_v-1 * t_v-2 -> s_v-1
%(op)% = \ (var x : s, var y : t) .! (var x : s) as s_v1
__when__else__
: forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%
bottom : forall p : Pcpo . p_v-1 %(fun)%
def : forall s : Type . Pred s_v-1@(s_v-1 ->? Unit) %(op)%
def__ : forall a : Type . a_v-1 ->? Unit %(fun)%
eq : forall s : Type . s_v-1 * s_v-1 ->? Unit %(pred)%
false
: bool %(construct bool)%
: Unit ->? Unit %(pred)%
: Unit %(fun)%
fst
: forall s : Type; t : Type . s_v-1 * t_v-2 -> s_v-1
%(op)% = \ (var x : s, var y : t) .! (var x : s) as s_v1
isBound
: forall c : Cpo . c_v-1 * (nat -> c_v-1) ->? Unit
%(pred)%
= \ (var x : c, var s : nat -> c)
. (all (\ n : nat . s (n) <<= x)) as Unit
isChain
: forall c : Cpo . (nat -> c_v-1) ->? Unit
%(pred)%
= \ (var s : nat -> c)
. (all (\ n : nat . s (n) <<= s (Suc (n)))) as Unit
not : Unit ->? Unit %(pred)%
not__ : ? Unit ->? Unit %(fun)%
sup : forall c : Cpo . (nat -> c_v-1) ->? c_v-1 %(op)%
true
: bool %(construct bool)%
: Unit ->? Unit %(pred)%
: Unit %(fun)%
tt : forall s : Type . Pred s_v-1@(s_v-1 ->? Unit) %(op)%
undefined
: forall p : Pcpo; c : Cpo . c_v-2 --> p_v-1
%(op)%
= (((fun Y[(c --> p)]
: forall p : Pcpo . (p_v-1 --> p_v-1) --> p_v-1) :
((c --> p) --> (c --> p)) --> (c --> p))
(((\ (var x' : _var_284_v284 --> p_v197)
. (var x' : _var_284_v284 --> p_v197)) :
(_var_284_v284 --> p) ->? (_var_284_v284 --> p)) as
(c --> p) --> c --> p) :
(c --> p)) as
_var_284_v284 --> p_v197
�__ : ? Unit ->? Unit %(fun)%
%% Variables -------------------------------------------------------------
f : p --> p
g : c --> d
x : p
x1 : c
x2 : c
y1 : d
y2 : d
%% Sentences -------------------------------------------------------------
program (op def[s]
: forall s : Type . Pred s_v-1@(s_v-1 ->? Unit)) :
Pred s@(s ->? Unit)
= (\ (var x : s) : s . ()) : s ->? Unit %(pe_def)%
program (op tt[s]
: forall s : Type . Pred s_v-1@(s_v-1 ->? Unit)) :
Pred s@(s ->? Unit)
= (\ (var x : s) : s . ()) : s ->? Unit %(pe_tt)%
forall x : s; y : t
. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)
((op __res__ : forall s : Type; t : Type . s_v-1 * t_v-2 -> s_v-1)
(var x : s, var y : t),
(var x : s) as s_v1) %(def___res__)%
forall x : s; y : t
. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)
((op fst : forall s : Type; t : Type . s_v-1 * t_v-2 -> s_v-1)
(var x : s, var y : t),
(var x : s) as s_v1) %(def_fst)%
((fun __=__[((s * _var_37_v37) ->? _var_33_v33)]
: forall s : Type . s_v-1 * s_v-1 ->? Unit) :
((s * _var_37_v37) ->? _var_33_v33) *
((s * _var_37_v37) ->? _var_33_v33) ->? Unit)
((\ ((var x : s) : s, var y : _var_37_v37) . def (x res y)) :
(s * _var_37_v37) ->? _var_33_v33,
(\ ((var x : s) : s, var y : _var_37_v37) . (def y) und (def x)) :
(s * _var_37_v37) ->? _var_33_v33) :
Unit
((fun __=__[((_var_73_v73 * _var_71_v71) -> _var_73_v73)]
: forall s : Type . s_v-1 * s_v-1 ->? Unit) :
((_var_73_v73 * _var_71_v71) -> _var_73_v73) *
((_var_73_v73 * _var_71_v71) -> _var_73_v73) ->? Unit)
((op fst[_var_73_v73; _var_71_v71]
: forall s : Type; t : Type . s_v-1 * t_v-2 -> s_v-1) :
_var_73_v73 * _var_71_v71 -> _var_73_v73,
(op __res__[_var_73_v73; _var_71_v71]
: forall s : Type; t : Type . s_v-1 * t_v-2 -> s_v-1) :
_var_73_v73 * _var_71_v71 -> _var_73_v73) :
Unit
((fun __=__[(s ->? Unit)]
: forall s : Type . s_v-1 * s_v-1 ->? Unit) :
(s ->? Unit) * (s ->? Unit) ->? Unit)
((\ (var x : s) : s
. ((pred eq[s] : forall s : Type . s_v-1 * s_v-1) : s * s ->? Unit)
(var x : s, var x : s) :
Unit) :
s ->? Unit,
(op tt[s] : forall s : Type . Pred s_v-1@(s_v-1 ->? Unit)) :
Pred s@(s ->? Unit)) :
Unit
((fun __=__[((s * s) ->? s)]
: forall s : Type . s_v-1 * s_v-1 ->? Unit) :
((s * s) ->? s) * ((s * s) ->? s) ->? Unit)
((\ (var x : s, var y : s)
. ((op __res__[s; Unit]
: forall s : Type; t : Type . s_v-1 * t_v-2 -> s_v-1) :
s * Unit -> s)
(var x : s,
((pred eq[s] : forall s : Type . s_v-1 * s_v-1) : s * s ->? Unit)
(var x : s, var y : s) :
Unit) :
s) :
(s * s) ->? s,
(\ (var x : s, var y : s)
. ((op __res__[s; Unit]
: forall s : Type; t : Type . s_v-1 * t_v-2 -> s_v-1) :
s * Unit -> s)
(var y : s,
((pred eq[s] : forall s : Type . s_v-1 * s_v-1) : s * s ->? Unit)
(var x : s, var y : s) :
Unit) :
s) :
(s * s) ->? s) :
Unit
forall s : nat -> c
. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)
((pred isChain : forall c : Cpo . nat -> c_v-1)(var s : nat -> c),
(all (\ n : nat . s (n) <<= s (Suc (n)))) as Unit) %(def_isChain)%
forall x : c; s : nat -> c
. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)
((pred isBound : forall c : Cpo . c_v-1 * (nat -> c_v-1))
(var x : c, var s : nat -> c),
(all (\ n : nat . s (n) <<= x)) as Unit) %(def_isBound)%
((fun __=__[p] : forall s : Type . s_v-1 * s_v-1 ->? Unit) :
p * p ->? Unit)
((var f : p --> p)
(((fun Y[p] : forall p : Pcpo . (p_v-1 --> p_v-1) --> p_v-1) :
(p --> p) --> p)
(var f : p --> p) :
p) :
p,
((fun Y[p] : forall p : Pcpo . (p_v-1 --> p_v-1) --> p_v-1) :
(p --> p) --> p)
(var f : p --> p) :
p) :
Unit
(fun __=>__ : Unit * Unit ->? Unit)
(((fun __=__[p] : forall s : Type . s_v-1 * s_v-1 ->? Unit) :
p * p ->? Unit)
((var f : p --> p)(var x : p) : p, var x : p) :
Unit,
((pred __<<=__[p] : forall c : Cpo . c_v-1 * c_v-1) :
p * p ->? Unit)
(((fun Y[p] : forall p : Pcpo . (p_v-1 --> p_v-1) --> p_v-1) :
(p --> p) --> p)
(var f : p --> p) :
p,
var x : p) :
Unit) :
Unit
(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)
(op undefined : forall p : Pcpo; c : Cpo . c_v-2 --> p_v-1,
(((fun Y[(c --> p)]
: forall p : Pcpo . (p_v-1 --> p_v-1) --> p_v-1) :
((c --> p) --> (c --> p)) --> (c --> p))
(((\ (var x' : _var_284_v284 --> p_v197)
. (var x' : _var_284_v284 --> p_v197)) :
(_var_284_v284 --> p) ->? (_var_284_v284 --> p)) as
(c --> p) --> c --> p) :
(c --> p)) as
_var_284_v284 --> p_v197) %(def_undefined)%
free type bool
::= true : bool
false : bool %(ga_bool)%
%% Diagnostics -----------------------------------------------------------
*** Warning 4.7, void universe class declaration 'Type'
*** Hint 6.5, is type variable 's'
*** Hint 6.7, is type variable 't'
*** Hint 11.6, redeclared type 'Unit'
*** Error, illegal type pattern argument '__'
*** Error, illegal type pattern argument '__'
*** Warning 17.6, ignoring declaration for builtin identifier 'true'
*** Warning 17.12, ignoring declaration for builtin identifier 'false'
*** Warning 19.9, ignoring declaration for builtin identifier '__/\__'
*** Warning 19.17, ignoring declaration for builtin identifier '__\/__'
*** Warning 19.25, ignoring declaration for builtin identifier '__=>__'
*** Warning 19.33, ignoring declaration for builtin identifier '__if__'
*** Warning 19.40, ignoring declaration for builtin identifier '__<=>__'
*** Warning 22.8, ignoring declaration for builtin identifier '__=__'
*** Hint 27.8, redeclared type '__->?__'
*** Hint 30.8, redeclared type '__*__'
*** Error, illegal type pattern '__ * __ * __'
*** Hint 40.7, not a class 's'
*** Hint 42.16, rebound variable 'x'
*** Hint 44.15, rebound variable 'x'
*** Error 46.11, unexpected mixfix token: und
*** Hint 50.8, redeclared type '__->__'
*** Hint 52.8, redeclared type '__->__'
*** Hint, repeated supertype '__->?__'
*** Error 54.47-54.49, ambiguous mixfix term
def__(f(x))
def(f)(x)
*** Error 54.32, unexpected mixfix token: all
*** Error 54.6, unexpected mixfix token: :
*** Hint 58.13, rebound variable 'x'
*** Hint 59.9, rebound variable 'x'
*** Warning 60.30, trying hard to find lazy type for 'program snd(x : s_v1, var y : t_v2) : t_v2 = y'
*** Hint 60.9, no type match for: snd
with (maximal) type: _var_11_v11 ->? t_v2
known types:
*** Hint 60.13-60.21, untypable application (with result type: t_v2)
'snd(x : s_v1, var y : t_v2)'
*** Error 60.30, no typing for 'program snd(x : s_v1, var y : t_v2) : t_v2 = y'
*** Error 65.22-65.30, ambiguous mixfix term
def(__res__(x, y))
def__(__res__(x, y))
*** Error 65.59, unexpected mixfix token: und
*** Hint 65.7, rebound variable 'x'
*** Error, unexpected term 'def (x res y)'
*** Hint 65.40, rebound variable 'x'
*** Error, unexpected term '(def y) und (def x)'
*** Hint 74.5, rebound variable 'x'
*** Hint 75.6, rebound variable 'x'
*** Hint 75.35, rebound variable 'x'
*** Warning 85.6, new type shadows type variable 's'
*** Warning 87.38, trying hard to find lazy type for 'program all(var p : s ->? Unit) : Unit ->? Unit = eq(p, tt)'
*** Hint 87.9, no type match for: all
with (maximal) type: _var_187_v187 ->? Unit ->? Unit
known types:
*** Hint 87.13-87.15, untypable application (with result type: Unit ->? Unit)
'all(var p : s ->? Unit)'
*** Error 87.38, no typing for 'program all(var p : s ->? Unit) : Unit ->? Unit = eq(p, tt)'
*** Error 90.45, unexpected mixfix token: t1
*** Error 93.11, unexpected mixfix token: impl
*** Error 93.58, unexpected mixfix token: And
*** Error 95.11, unexpected mixfix token: or
*** Error 96.21, unexpected mixfix token: impl
*** Error 95.48, unexpected mixfix token: all
*** Error 99.32, unexpected mixfix token: impl
*** Error 99.17, unexpected mixfix token: all
*** Error 98.39, unexpected mixfix token: all
*** Error 101.29, unexpected mixfix token: all
*** Error 103.44, unexpected mixfix token: impl
*** Error 108.51, unexpected mixfix token: impl
*** Error 108.22, unexpected mixfix token: all
*** Error 108.3, unexpected mixfix token: all
*** Hint 117.5, is type variable 'c'
*** Error 121.3, unexpected mixfix token: all
*** Error 122.31, unexpected mixfix token: und
*** Error 122.3, unexpected mixfix token: all
*** Error 123.31, unexpected mixfix token: und
*** Error 123.3, unexpected mixfix token: all
*** Error 125.55, unexpected mixfix token: Suc
*** Error 125.32, unexpected mixfix token: all
*** Error, unexpected term 'all (\ n : nat . s (n) <<= s (Suc (n)))'
*** Hint 126.15, rebound variable 'x'
*** Error 126.38, unexpected mixfix token: all
*** Error, unexpected term 'all (\ n : nat . s (n) <<= x)'
*** Error 131.56, unexpected mixfix token: impl
*** Error 130.32, unexpected mixfix token: impl
*** Error 130.3, unexpected mixfix token: all
*** Error 134.31, unexpected mixfix token: impl
*** Error 134.3, unexpected mixfix token: all
*** Hint 139.5, is type variable 'p'
*** Warning 141.4, ignoring declaration for builtin identifier 'bottom'
*** Error 143.3, unexpected mixfix token: all
*** Hint 148.6, is type variable 'f'
*** Error 150.15, unexpected mixfix token: [
*** Hint 153.5, is type variable 'c'
*** Hint 153.5, rebound type variable 'c'
*** Hint 153.8, is type variable 'd'
*** Hint 157.7, not a class 'c'
*** Hint 157.11, not a class 'c'
*** Hint 157.18, not a class 'd'
*** Hint 157.23, not a class 'd'
*** Error 159.45, unexpected mixfix token: und
*** Hint 169.9, redeclared type '__-->?__'
*** Hint, repeated supertype '__->?__'
*** Error 171.35, unexpected mixfix token: und
*** Error 174.45, unexpected mixfix token: +
*** Error 173.40, unexpected mixfix token: und
*** Error 172.39, unexpected mixfix token: und
*** Error 171.9, unexpected mixfix token: all
*** Error 170.7, unexpected mixfix token: :
*** Error 176.51, unexpected mixfix token: impl
*** Error 176.31, unexpected mixfix token: all
*** Error 181.9, non-unique kind for '__-->__'
*** Hint, repeated supertype '__-->?__'
*** Error 182.51-182.53, ambiguous mixfix term
def__(f(x))
def(f)(x)
*** Error 182.36, unexpected mixfix token: all
*** Error 182.7, unexpected mixfix token: :
*** Hint 184.7, not a kind 'c --> d'
*** Hint 184.11, not a kind 'c --> d'
*** Error 186.26, unexpected mixfix token: c
*** Error 193.32, unexpected mixfix token: impl
*** Error 192.40, unexpected mixfix token: und
*** Error 192.3, unexpected mixfix token: all
*** Hint 195.7, not a kind 'p --> p'
*** Hint 195.5, rebound variable 'f'
*** Hint 195.20, not a class 'p'
*** Hint 195.18, rebound variable 'x'
*** Hint 199.14-199.24, unable to prove: c < _var_284_v284
*** Error 199.14-199.24, in term'(((fun Y[(c --> p)]
: forall p : Pcpo . (p_v-1 --> p_v-1) --> p_v-1) :
((c --> p) --> (c --> p)) --> (c --> p))
(((\ (var x' : _var_284_v284 --> p_v197)
. (var x' : _var_284_v284 --> p_v197)) :
(_var_284_v284 --> p) ->? (_var_284_v284 --> p)) as
(c --> p) --> c --> p) :
(c --> p)) as
_var_284_v284 --> p_v197' of type '_var_284_v284 --> p_v197'
unresolved constraints '{ c < _var_284_v284 }'
*** Warning 204.20, ignoring declaration for builtin identifier 'true'
*** Warning 204.27, ignoring declaration for builtin identifier 'false'