9 consts |
9 consts |
10 conj :: "[plf,plf] => plf" (infixr "&" 35) |
10 conj :: "[plf,plf] => plf" (infixr "&" 35) |
11 disj :: "[plf,plf] => plf" (infixr "|" 35) |
11 disj :: "[plf,plf] => plf" (infixr "|" 35) |
12 impl :: "[plf,plf] => plf" (infixr ">" 35) |
12 impl :: "[plf,plf] => plf" (infixr ">" 35) |
13 eq :: "[plf,plf] => plf" (infixr "=" 35) |
13 eq :: "[plf,plf] => plf" (infixr "=" 35) |
14 ff :: "plf" |
14 ff :: "plf" ("ff") |
15 |
15 |
16 PL :: "plf => o" ("[* / _ / *]" [] 100) |
16 PL :: "plf => o" ("[* / _ / *]" [] 100) |
17 |
17 |
18 syntax |
18 syntax |
19 "_NG" :: "plf => plf" ("- _ " [50] 55) |
19 "_NG" :: "plf => plf" ("- _ " [50] 55) |
20 |
20 |
21 translations |
21 translations |
22 |
22 |
23 "[* A & B *]" == "[*A*] && [*B*]" |
23 "[* A & B *]" == "[*A*] && [*B*]" |
24 "[* A | B *]" == "![*A*] ++ ![*B*]" |
24 "[* A | B *]" == "![*A*] ++ ![*B*]" |
25 "[* - A *]" == "[*A > CONST ff*]" |
25 "[* - A *]" == "[*A > ff*]" |
26 "[* XCONST ff *]" == "0" |
26 "[* ff *]" == "0" |
27 "[* A = B *]" => "[* (A > B) & (B > A) *]" |
27 "[* A = B *]" => "[* (A > B) & (B > A) *]" |
28 |
28 |
29 "[* A > B *]" == "![*A*] -o [*B*]" |
29 "[* A > B *]" == "![*A*] -o [*B*]" |
30 |
30 |
31 (* another translations for linear implication: |
31 (* another translations for linear implication: |