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
27
28
29
30
31
32
33
34
35
36
37
38
|
fmod BAR{Y :: T} is
sorts Y$Elt Bool X$Foo .
subsort X$Foo < Y$Elt .
op if_then_else_fi : Bool Universal Universal -> Universal [poly (2 3 0) prec
0 gather (& & &) special (
id-hook BranchSymbol
term-hook 1 (true)
term-hook 2 (false))] .
op _==_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
special (
id-hook EqualitySymbol
term-hook equalTerm (true)
term-hook notEqualTerm (false))] .
op _=/=_ : Universal Universal -> Bool [poly (1 2) prec 51 gather (E E)
special (
id-hook EqualitySymbol
term-hook equalTerm (false)
term-hook notEqualTerm (true))] .
op true : -> Bool [ctor special (
id-hook SystemTrue)] .
op false : -> Bool [ctor special (
id-hook SystemFalse)] .
op _and_ : Bool Bool -> Bool [assoc comm prec 55 gather (e E)] .
op _or_ : Bool Bool -> Bool [assoc comm prec 59 gather (e E)] .
op _xor_ : Bool Bool -> Bool [assoc comm prec 57 gather (e E)] .
op not_ : Bool -> Bool [prec 53 gather (E)] .
op _implies_ : Bool Bool -> Bool [prec 61 gather (e E)] .
eq true and A:Bool = A:Bool .
eq false and A:Bool = false .
eq A:Bool and A:Bool = A:Bool .
eq false xor A:Bool = A:Bool .
eq A:Bool xor A:Bool = false .
eq A:Bool and (B:Bool xor C:Bool) = A:Bool and B:Bool xor A:Bool and C:Bool .
eq not A:Bool = true xor A:Bool .
eq A:Bool or B:Bool = A:Bool and B:Bool xor A:Bool xor B:Bool .
eq A:Bool implies B:Bool = not (A:Bool xor A:Bool and B:Bool) .
endfm
Bye.
|
