bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maederclass Eq < Type

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maederclass Ord < Eq

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maedertype a : Ord

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maederop f : forall e : Ord . e -> e

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederop c : a

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder. (fun __=__[a] : forall a : Type . a_v-1 * a_v-1 ->? Unit)

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder ((op f[a] : forall e : Ord . e_v-1 -> e_v-1)

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder ((op f[a] : forall e : Ord . e_v-1 -> e_v-1)(op c : a)),

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder op c : a)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertype t : Eq

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maederop b : t

488aed6214197096d0e23c9bbd614263b11a543bJonathan von Schroeder. (fun __=__[t] : forall a : Type . a_v-1 * a_v-1 ->? Unit)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ((op f[t] : forall e : Ord . e_v-1 -> e_v-1)(op b : t), op b : t)

488aed6214197096d0e23c9bbd614263b11a543bJonathan von Schroeder%% Classes ---------------------------------------------------------------

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian MaederEq < Type

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian MaederOrd < Eq

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder%% Type Constructors -----------------------------------------------------

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian MaederLogical : Type := Unit ->? Unit

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian MaederPred : Type -> Type := \ a : Type . a_v-1 ->? Unit

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian MaederUnit : Type := Unit

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder__*__ : Type+ -> Type+ -> Type

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder__-->__ : Type- -> Type+ -> Type

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder__-->?__ : Type- -> Type+ -> Type

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder__->__ : Type- -> Type+ -> Type

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder__->?__ : Type- -> Type+ -> Type

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maedera : Ord

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maedert : Eq

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder%% Assumptions -----------------------------------------------------------

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder__/\__ : Unit * Unit ->? Unit %(fun)%

bf059a1d954c7e4d74f45ca0822e2f41709a0149Christian Maeder__<=>__ : Unit * Unit ->? Unit %(fun)%

__=__ : forall a : Type . a_v-1 * a_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)%

__when__else__

: forall a : Type . a_v-1 * Unit * a_v-1 ->? a_v-1 %(fun)%

b : t %(op)%

bottom : forall a : Type . a_v-1 %(fun)%

c : a %(op)%

def__ : forall a : Type . a_v-1 ->? Unit %(fun)%

f : forall e : Ord . e_v-1 -> e_v-1 %(op)%

false : Unit %(fun)%

not__ : Unit ->? Unit %(fun)%

true : Unit %(fun)%

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

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

(fun __=__[a] : forall a : Type . a_v-1 * a_v-1 ->? Unit)

((op f[a] : forall e : Ord . e_v-1 -> e_v-1)

((op f[a] : forall e : Ord . e_v-1 -> e_v-1)(op c : a)),

op c : a)

(fun __=__[t] : forall a : Type . a_v-1 * a_v-1 ->? Unit)

((op f[t] : forall e : Ord . e_v-1 -> e_v-1)(op b : t), op b : t)

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

*** Error 14.8, unresolved constraint 't : Ord'

*** Hint 16.7,

expected: Ord

found: Eq