equal
deleted
inserted
replaced
10 W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers, |
10 W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers, |
11 1966. |
11 1966. |
12 *) |
12 *) |
13 |
13 |
14 QPair = Sum + |
14 QPair = Sum + |
15 |
|
16 global |
|
17 |
15 |
18 consts |
16 consts |
19 QPair :: [i, i] => i ("<(_;/ _)>") |
17 QPair :: [i, i] => i ("<(_;/ _)>") |
20 qfst,qsnd :: i => i |
18 qfst,qsnd :: i => i |
21 qsplit :: [[i, i] => 'a, i] => 'a::logic (*for pattern-matching*) |
19 qsplit :: [[i, i] => 'a, i] => 'a::logic (*for pattern-matching*) |
32 |
30 |
33 translations |
31 translations |
34 "QSUM x:A. B" => "QSigma(A, %x. B)" |
32 "QSUM x:A. B" => "QSigma(A, %x. B)" |
35 "A <*> B" => "QSigma(A, _K(B))" |
33 "A <*> B" => "QSigma(A, _K(B))" |
36 |
34 |
37 local |
|
38 |
35 |
39 defs |
36 defs |
40 QPair_def "<a;b> == a+b" |
37 QPair_def "<a;b> == a+b" |
41 qfst_def "qfst(p) == THE a. EX b. p=<a;b>" |
38 qfst_def "qfst(p) == THE a. EX b. p=<a;b>" |
42 qsnd_def "qsnd(p) == THE b. EX a. p=<a;b>" |
39 qsnd_def "qsnd(p) == THE b. EX a. p=<a;b>" |