1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
set show timing off .
set show advisories off .
select META-MODULE .
red (subsort 'Foo < 'Bar .) .
red (op 'f : 'Foo -> 'Bar [none] .) .
red (ceq 'f['X:Foo] = 'a.Bar if 'g['a.Foo,'Y:Foo] := 'X:Foo [none] .) .
red 'g['a.Foo,'Y:Foo] := 'X:Foo .
red
(fmod 'FOO is
including 'MACHINE-INT .
sorts 'Foo ; 'Bar .
subsort 'Foo < 'Bar .
op 'f : 'Foo -> 'Bar [none] .
op 'g : '`[Bar`] -> '`[Bar`] [none] .
cmb 'X:Bar : 'Foo if 'f['Y:Bar] := 'f['X:Bar] /\
'g['Y:Bar, 'a.Foo] = 'a.Foo [none] .
eq 'f['X:Foo] = 'g['a.Foo,'X:Foo] [none] .
ceq 'f['X:Foo] = 'a.Bar if 'g['a.Foo,'Y:Foo] := 'X:Foo [none] .
endfm)
.
red (fmod 'FOO is including 'MACHINE-INT . sorts 'Foo ; 'Bar .
subsort 'Foo < 'Bar . op 'f : 'Foo -> 'Bar[none]. op 'g : '`[Bar`] ->
'`[Bar`][none]. none eq 'f['X:Foo] = 'g['a.Foo,'X:Foo] [none] . endfm).
|
