11 1966. |
11 1966. |
12 *) |
12 *) |
13 |
13 |
14 QPair = Sum + "simpdata" + |
14 QPair = Sum + "simpdata" + |
15 consts |
15 consts |
16 QPair :: "[i, i] => i" ("<(_;/ _)>") |
16 QPair :: [i, i] => i ("<(_;/ _)>") |
17 qfst,qsnd :: "i => i" |
17 qfst,qsnd :: i => i |
18 qsplit :: "[[i, i] => 'a, i] => 'a::logic" (*for pattern-matching*) |
18 qsplit :: [[i, i] => 'a, i] => 'a::logic (*for pattern-matching*) |
19 qconverse :: "i => i" |
19 qconverse :: i => i |
20 QSigma :: "[i, i => i] => i" |
20 QSigma :: [i, i => i] => i |
21 |
21 |
22 "<+>" :: "[i,i]=>i" (infixr 65) |
22 "<+>" :: [i,i]=>i (infixr 65) |
23 QInl,QInr :: "i=>i" |
23 QInl,QInr :: i=>i |
24 qcase :: "[i=>i, i=>i, i]=>i" |
24 qcase :: [i=>i, i=>i, i]=>i |
25 |
25 |
26 syntax |
26 syntax |
27 "@QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10) |
27 "@QSUM" :: [idt, i, i] => i ("(3QSUM _:_./ _)" 10) |
28 "<*>" :: "[i, i] => i" (infixr 80) |
28 "<*>" :: [i, i] => i (infixr 80) |
29 |
29 |
30 translations |
30 translations |
31 "QSUM x:A. B" => "QSigma(A, %x. B)" |
31 "QSUM x:A. B" => "QSigma(A, %x. B)" |
32 "A <*> B" => "QSigma(A, _K(B))" |
32 "A <*> B" => "QSigma(A, _K(B))" |
33 |
33 |