ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Eq < Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederclass Ord < Eq

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedertype a : Ord

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederop c : a

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder ((op f[a] : forall e : Ord . e -> e)

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder op c : a)

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedertype t : Eq

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederop b : t

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

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Classes ---------------------------------------------------------------

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederEq < Type

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederOrd < Eq

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Type Constructors -----------------------------------------------------

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederLogical : Type := Unit ->? Unit

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederPred : Type -> Type := \ a : Type . a ->? Unit

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaederUnit : Type := Unit

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__-->__ : Type- -> Type+ -> Type

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__->__ : Type- -> Type+ -> Type

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedera : Ord

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedert : Eq

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Assumptions -----------------------------------------------------------

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

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__=__ : forall a : Type . a * a ->? Unit %(fun)%

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__=e=__ : forall a : Type . a * a ->? Unit %(fun)%

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__if__ : Unit * Unit ->? Unit %(fun)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder__when__else__ : forall a : Type . a * Unit * a ->? a %(fun)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederb : t %(op)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederbottom : forall a : Type . a %(fun)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederc : a %(op)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederdef__ : forall a : Type . a ->? Unit %(fun)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederf : forall e : Ord . e -> e %(op)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederfalse : Unit %(fun)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedernot__ : Unit ->? Unit %(fun)%

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedertrue : Unit %(fun)%

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Sentences -------------------------------------------------------------

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder ((op f[a] : forall e : Ord . e -> e)

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder op c : a)

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

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

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder%% Diagnostics -----------------------------------------------------------

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