329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder%% predefined universe containing all types,

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner%% superclass of all other classes

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maederclass Type < Type

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maedervar s : Type; t : Type

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder%% invisible type "Unit" for formulae

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maedertype Unit

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder %% flat cpo with bottom

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder %% type aliases

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maederpred true, false : Unit

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maederpred __/\__, __\/__, __=>__, __if__, __<=>__ : Unit * Unit

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maederpred not : Unit

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maederpred __=__ : s * s

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder %% =e=

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder %% (builtin) type (constructors)

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maedertype __->?__ : Type- -> Type+ -> Type

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder%% nested pairs are different from n-tupels (n > 2)

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maedertype __*__ : Type+ -> Type+ -> Type

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder%% ...

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder%% "pred p args = e" abbreviates "op p args :? unit = e"

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder%% CASL requires "<=>" for pred-defn and disallows "()" as result

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maederop def, tt : Pred s

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maedervar x : s

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maederprogram (op def[s]

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder : forall s : Type . Pred s_v-1@(s_v-1 ->? Unit)) :

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder Pred s@(s ->? Unit)

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder = (\ (var x : s) . ()) : s ->? Unit

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder %% def is also total (identical to tt)

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maederprogram (op tt[s]

1aa11f4e4b984f2a6d6ce9700cbe82283c8d196aChristian Maeder : forall s : Type . Pred s_v-1@(s_v-1 ->? Unit)) :

1aa11f4e4b984f2a6d6ce9700cbe82283c8d196aChristian Maeder Pred s@(s ->? Unit)

c8ecc5578d32b222f35b625d4dfe7a3fd8bb4173Christian Maeder = (\ (var x : s) . ()) : s ->? Unit

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder %% tt is total "op tt(x: s): unit = ()"

329c739bc05b8ce8d54f81071d0826ff771d1f78Christian Maeder%% total function type

51b1633dc0785a542da974fae21fa7d6622c934eChristian Maedertype __->__ : Type- -> Type+ -> Type

51b1633dc0785a542da974fae21fa7d6622c934eChristian Maedertype __->__ < __->?__

51b1633dc0785a542da974fae21fa7d6622c934eChristian Maeder%% total functions

51b1633dc0785a542da974fae21fa7d6622c934eChristian Maederop __res__ : forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1

51b1633dc0785a542da974fae21fa7d6622c934eChristian Maeder = \ (var x : s, var y : t) .! (var x : s) as s_v1

51b1633dc0785a542da974fae21fa7d6622c934eChristian Maederop fst : forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1

51b1633dc0785a542da974fae21fa7d6622c934eChristian Maeder = \ (var x : s, var y : t) .! (var x : s) as s_v1

51b1633dc0785a542da974fae21fa7d6622c934eChristian Maeder%% trivial because its the strict function property

. ((fun __=__[_var_22_v22 * _var_23_v23 ->? _var_22_v22]

: forall s : Type . s_v-1 * s_v-1 ->? Unit) :

(_var_22_v22 * _var_23_v23 ->? _var_22_v22) *

(_var_22_v22 * _var_23_v23 ->? _var_22_v22) ->? Unit)

((op fst[_var_22_v22; _var_23_v23]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1) :

_var_22_v22 * _var_23_v23 ->? _var_22_v22,

(op __res__[_var_22_v22; _var_23_v23]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1) :

_var_22_v22 * _var_23_v23 ->? _var_22_v22) :

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)

. ((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;

pred isBound : forall c : Cpo . c_v-1 * (nat -> c_v-1);

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

type __-->__ < __-->?__

var f : c --> d; g : c --> d

type instance __-->__ : Cpo- -> Pcpo+ -> Pcpo

op undefined : forall c : Cpo; p : Pcpo . c_v-1 -->? p_v-2

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% 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

__*__

: (Cpo+ -> Cpo+ -> Cpo, Pcpo+ -> Pcpo+ -> Pcpo,

Type+ -> Type+ -> Type)

__-->__

: (Cpo- -> Cpo+ -> Cpo, Cpo- -> Cpo+ -> Pcpo,

Cpo- -> Pcpo+ -> Pcpo, Type- -> Type+ -> Type) < (__-->?__,

__-->?__, __->__)

__-->?__ : (Cpo- -> Cpo+ -> Pcpo, Type- -> Type+ -> Type) < __->?__

__->__ : Type- -> Type+ -> Type < __->?__

__->?__ : Type- -> Type+ -> Type

bool

: Flatcpo

%[free type bool

::= true : bool

false : bool]%

c : Cpo %(var_155)%

d : Cpo %(var_160)%

f : Flatcpo %(var_159)%

nat : Flatcpo

p : Pcpo %(var_158)%

s : Type %(var_1)%

t : Type %(var_2)%

%% Assumptions -----------------------------------------------------------

__/\__ : 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)%

f : c --> d %(var)%

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

g : c --> d %(var)%

isBound : forall c : Cpo . c_v-1 * (nat -> c_v-1) ->? Unit %(pred)%

isChain : forall c : Cpo . (nat -> c_v-1) ->? Unit %(pred)%

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 c : Cpo; p : Pcpo . c_v-1 -->? p_v-2 %(op)%

x : s %(var)%

x1 : c %(var)%

x2 : c %(var)%

y1 : d %(var)%

y2 : d %(var)%

�__ : ? Unit ->? Unit %(fun)%

%% Sentences -------------------------------------------------------------

program (op def[s]

: forall s : Type . Pred s_v-1@(s_v-1 ->? Unit)) :

Pred s@(s ->? Unit)

= (\ (var x : 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 ->? 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 __=__[_var_22_v22 * _var_23_v23 ->? _var_22_v22]

: forall s : Type . s_v-1 * s_v-1 ->? Unit) :

(_var_22_v22 * _var_23_v23 ->? _var_22_v22) *

(_var_22_v22 * _var_23_v23 ->? _var_22_v22) ->? Unit)

((op fst[_var_22_v22; _var_23_v23]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1) :

_var_22_v22 * _var_23_v23 ->? _var_22_v22,

(op __res__[_var_22_v22; _var_23_v23]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1) :

_var_22_v22 * _var_23_v23 ->? _var_22_v22) :

Unit

((fun __=__[s ->? Unit]

: forall s : Type . s_v-1 * s_v-1 ->? Unit) :

(s ->? Unit) * (s ->? Unit) ->? Unit)

((\ (var x : 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

free type bool

::= true : bool

false : bool %(ga_bool)%

%% Diagnostics -----------------------------------------------------------

*** Error 4.7, illegal 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 '__'

*** Error 17.6, illegal overloading of predefined identifier 'true'

*** Error 17.12, illegal overloading of predefined identifier 'false'

*** Error 19.9, illegal overloading of predefined identifier '__/\__'

*** Error 19.17, illegal overloading of predefined identifier '__\/__'

*** Error 19.25, illegal overloading of predefined identifier '__=>__'

*** Error 19.33, illegal overloading of predefined identifier '__if__'

*** Error 19.40, illegal overloading of predefined identifier '__<=>__'

*** Error 22.8, illegal overloading of predefined identifier '__=__'

*** Hint 27.8, redeclared type '__->?__'

*** Hint 30.8, redeclared type '__*__'

*** Error, illegal type pattern '__ * __ * __'

*** Hint 42.16, variable shadows global name(s) 'x'

*** Hint 44.15, variable shadows global name(s) '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, variable shadows global name(s) 'x'

*** Hint 59.9, variable shadows global name(s) 'x'

*** Hint 60.9, no type match for: snd

with (maximal) type: _var_11_v11 ->? t

known types:

*** Hint 60.13-60.21, untypable application (with result type: t)

'snd(x : s, var y : t)'

*** Error 60.30, no typing for 'program snd(x : s, var y : t) : t = 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 66.9-66.16, in type of '((op fst[_var_24_v24; _var_25_v25]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1) :

_var_24_v24 * _var_25_v25 ->? _var_24_v24,

(op __res__[_var_26_v26; _var_27_v27]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1) :

_var_26_v26 * _var_27_v27 ->? _var_26_v26)'

type '(_var_24_v24 * _var_25_v25 ->? _var_24_v24) *

(_var_26_v26 * _var_27_v27 ->? _var_26_v26)' (66.16)

is not unifiable with type 'Unit ->? _var_13_v13 * _var_13_v13' (66.16)

*** Hint 74.5, variable shadows global name(s) 'x'

*** Hint, in type of '(var x : s, var x : s)'

type 's * s'

is not unifiable with type 'Unit ->? _var_43_v43 * _var_43_v43' (74.17)

*** Hint 74.5, variable shadows global name(s) 'x'

*** Hint, in type of '(var x : s, var x : s)'

type 's * s'

is not unifiable with type 'Unit ->? _var_52_v52 * _var_52_v52' (74.17)

*** Hint 74.3-74.23, in type of '((\ (var x : s)

. ((pred eq[_var_52_v52] : forall s : Type . s_v-1 * s_v-1) :

_var_52_v52 * _var_52_v52 ->? Unit)

(var x : s, var x : s) :

Unit) :

_var_49_v49 ->? _var_50_v50,

(op tt[_var_55_v55]

: forall s : Type . Pred s_v-1@(s_v-1 ->? Unit)) :

Pred _var_55_v55@(_var_55_v55 ->? Unit))'

type '(s ->? Unit) * Pred _var_55_v55@(_var_55_v55 ->? Unit)' (74.23)

is not unifiable with type 'Unit ->? _var_37_v37 * _var_37_v37' (74.23)

*** Hint 75.6, variable shadows global name(s) 'x'

*** Hint, in type of '(var x : s, var y : s)'

type 's * s'

is not unifiable with type 'Unit ->? _var_75_v75 * _var_75_v75' (75.26)

*** Hint, in type of '(var x : s, var y : s)'

type 's * s'

is not unifiable with type 'Unit ->? _var_80_v80 * _var_80_v80' (75.26)

*** Hint 75.21-75.27, in type of '(var x : s,

((pred eq[_var_80_v80] : forall s : Type . s_v-1 * s_v-1) :

_var_80_v80 * _var_80_v80 ->? Unit)

(var x : s, var y : s) :

Unit)'

type 's * Unit' (75.27)

is not unifiable with type 'Unit ->? _var_69_v69 * _var_70_v70' (75.27)

*** Hint 75.35, variable shadows global name(s) 'x'

*** Hint, in type of '(var x : s, var y : s)'

type 's * s'

is not unifiable with type 'Unit ->? _var_94_v94 * _var_94_v94' (75.55)

*** Hint, in type of '(var x : s, var y : s)'

type 's * s'

is not unifiable with type 'Unit ->? _var_99_v99 * _var_99_v99' (75.55)

*** Hint 75.50-75.56, in type of '(var y : s,

((pred eq[_var_99_v99] : forall s : Type . s_v-1 * s_v-1) :

_var_99_v99 * _var_99_v99 ->? Unit)

(var x : s, var y : s) :

Unit)'

type 's * Unit' (75.56)

is not unifiable with type 'Unit ->? _var_88_v88 * _var_89_v89' (75.56)

*** Hint 75.6, variable shadows global name(s) 'x'

*** Hint, in type of '(var x : s, var y : s)'

type 's * s'

is not unifiable with type 'Unit ->? _var_117_v117 * _var_117_v117' (75.26)

*** Hint, in type of '(var x : s, var y : s)'

type 's * s'

is not unifiable with type 'Unit ->? _var_122_v122 * _var_122_v122' (75.26)

*** Hint 75.21-75.27, in type of '(var x : s,

((pred eq[_var_122_v122] : forall s : Type . s_v-1 * s_v-1) :

_var_122_v122 * _var_122_v122 ->? Unit)

(var x : s, var y : s) :

Unit)'

type 's * Unit' (75.27)

is not unifiable with type 'Unit ->? _var_111_v111 * _var_112_v112' (75.27)

*** Hint 75.35, variable shadows global name(s) 'x'

*** Hint, in type of '(var x : s, var y : s)'

type 's * s'

is not unifiable with type 'Unit ->? _var_136_v136 * _var_136_v136' (75.55)

*** Hint, in type of '(var x : s, var y : s)'

type 's * s'

is not unifiable with type 'Unit ->? _var_141_v141 * _var_141_v141' (75.55)

*** Hint 75.50-75.56, in type of '(var y : s,

((pred eq[_var_141_v141] : forall s : Type . s_v-1 * s_v-1) :

_var_141_v141 * _var_141_v141 ->? Unit)

(var x : s, var y : s) :

Unit)'

type 's * Unit' (75.56)

is not unifiable with type 'Unit ->? _var_130_v130 * _var_131_v131' (75.56)

*** Hint 75.3-75.57, in type of '((\ (var x : s, var y : s)

. ((op __res__[_var_111_v111; _var_112_v112]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1) :

_var_111_v111 * _var_112_v112 ->? _var_111_v111)

(var x : s,

((pred eq[_var_117_v117] : forall s : Type . s_v-1 * s_v-1) :

_var_117_v117 * _var_117_v117 ->? Unit)

(var x : s, var y : s) :

Unit) :

_var_111_v111) :

_var_108_v108 * _var_109_v109 ->? _var_107_v107,

(\ (var x : s, var y : s)

. ((op __res__[_var_130_v130; _var_131_v131]

: forall s : Type; t : Type . s_v-1 * t_v-2 ->? s_v-1) :

_var_130_v130 * _var_131_v131 ->? _var_130_v130)

(var y : s,

((pred eq[_var_136_v136] : forall s : Type . s_v-1 * s_v-1) :

_var_136_v136 * _var_136_v136 ->? Unit)

(var x : s, var y : s) :

Unit) :

_var_130_v130) :

_var_127_v127 * _var_128_v128 ->? _var_126_v126)'

type '(s * s ->? s) * (s * s ->? s)' (75.57)

is not unifiable with type 'Unit ->? _var_61_v61 * _var_61_v61' (75.57)

*** Hint 85.6, redeclared type 's'

*** Error 85.6, merge: TypeVarDefn of 's'

*** Error 85.10, illegal supertype for variable '? s_v1'

*** Hint 87.9, no type match for: all

with (maximal) type: _var_152_v152 ->? 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

*** Hint 126.15, variable shadows global name(s) 'x'

*** Error 126.38, unexpected mixfix token: all

*** 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'

*** Error 141.4, illegal overloading of predefined 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, redeclared type 'c'

*** Hint 153.8, is type variable '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 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: :

*** Error 186.26, unexpected mixfix token: c

*** Error, incompatible kind of: p_v158 -->? p_v158

expected: Cpo-

found: Type

*** Error 193.32, unexpected mixfix token: impl

*** Error 192.27, unexpected mixfix token: Y

*** Error 192.3, unexpected mixfix token: all

*** Error 195.27, unexpected mixfix token: Y

*** Error 200.20, illegal overloading of predefined identifier 'true'

*** Error 200.27, illegal overloading of predefined identifier 'false'