type s, t

op snd : s * t -> t

program (op snd : s * t -> t)(var x : s, var y : t) = (var y : t)

program (op snd : s * t -> t)(var x : s, var y : t) = (var y : t)

program (op snd : s * t -> t)(var x : s, var y : t) =

(var y : t) : t

program (op snd : s * t -> t)(var x : s, var y : t) : t =

(var y : t)

program (op snd : s * t -> t)(var x : s, var y : t) : t =

(var y : t)

program (op snd : s * t -> t)(var x : s, var y : t) : t =

(var y : t)

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

op a : s

program (var b : s) = (op a : s)

op b : s

program (op b : s) : s = (op a : s)

op x : s; y : t

op c : t = (op snd : s * t -> t)((op x : s) : s, (op y : t) : t)

%% Type Constructors -----------------------------------------------------

Logical : Type := Unit ->? Unit

Pred : Type -> Type := \ a : Type . a ->? Unit

Unit : Type := Unit

__*__ : Type+ -> Type+ -> Type

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

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

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

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

s : Type

t : Type

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

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

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

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

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

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

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

__if__ : Unit * Unit ->? Unit %(fun)%

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

a : s %(op)%

b : s %(op)%

bottom : forall a : Type . a %(fun)%

c : t

%(op)% = (op snd : s * t -> t)((op x : s) : s, (op y : t) : t)

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

false : Unit %(fun)%

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

snd : s * t -> t %(op)%

true : Unit %(fun)%

x : s %(op)%

y : t %(op)%

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

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

program (op snd : s * t -> t)(var x : s, var y : t) =

(var y : t) %(pe_snd)%

program (op snd : s * t -> t)(var x : s, var y : t) =

(var y : t) %(pe_snd)%

program (op snd : s * t -> t)(var x : s, var y : t) =

(var y : t) : t %(pe_snd)%

program (op snd : s * t -> t)(var x : s, var y : t) : t =

(var y : t) %(pe_snd)%

program (op snd : s * t -> t)(var x : s, var y : t) : t =

(var y : t) %(pe_snd)%

program (op snd : s * t -> t)(var x : s, var y : t) : t =

(var y : t) %(pe_snd)%

program (var b : s) = (op a : s) %(pe_b)%

program (op b : s) : s = (op a : s) %(pe_b)%

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

(op c : t,

(op snd : s * t -> t)((op x : s) : s, (op y : t) : t)) %(def_c)%

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

*** Error 14.10, illegal toplevel pattern '(var x : s, var y : s)'

*** Warning 17.9, illegal lhs pattern '(var b : s)'