HasCASL/test/PatternEq.hascasl

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
type s, t
op snd : s * t -> t
program snd (x, y) = y

program (snd (x, y)) = y
program (snd (x, y)) = y : t
program (snd (x, y)) : t = y


program snd (x, y) : t = y

program snd (x : s, y : t) : t = y

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

op a : s
program b:s = a
op b : s
program b:s = a

op x : s; y: t

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