PatternEq.hascasl.output revision af47051acb16b97b6bc0ff7295cae44eed87d63e
type s, t
op snd : s * 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) : 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)
op a : s
program (var b : s) = (op a : s)
op b : s
program (op b : s) = (op a : s)
op x : s; y : t
op c : t = ((op snd : s * t -> t)(op x : s, op y : t) : t) as t
%% Type Constructors -----------------------------------------------------
? : +Type -> Type
Logical : Type := ? Unit
Pred : -Type -> Type := \ a : -Type . a ->? Unit
Unit : Type
__*__ : +Type -> +Type -> Type
__*__*__ : +Type -> +Type -> +Type -> Type
__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type
__*__*__*__*__ : +Type -> +Type -> +Type -> +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, op y : t) : t) as 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 snd(var x : s, var y : t) : t = (var y : t) %(pe_snd)%
program snd(var x : s, var y : t) : t = (var y : t) %(pe_snd)%
program snd(var x : s, var y : t) : t = (var y : t) : t %(pe_snd)%
program snd(var x : s, var y : t) : t = (var y : t) %(pe_snd)%
program snd(var x : s, var y : t) : t = (var y : t) %(pe_snd)%
program snd(var x : s, var y : t) : t = (var y : t) %(pe_snd)%
program (var b : s) = a %(pe_b)%
program b = a %(pe_b)%
__=__(c, (snd(x, y) : t) as t) %(def_c)%
%% Diagnostics -----------------------------------------------------------
*** Error 14.11-14.18, illegal toplevel pattern '(var x : s, var y : s)'
*** Warning 17.10, illegal lhs pattern '(var b : s)'