38 Eqtype :: "[t,t]=>prop" ("(3_ =/ _)" [10,10] 5) |
38 Eqtype :: "[t,t]=>prop" ("(3_ =/ _)" [10,10] 5) |
39 Elem :: "[i, t]=>prop" ("(_ /: _)" [10,10] 5) |
39 Elem :: "[i, t]=>prop" ("(_ /: _)" [10,10] 5) |
40 Eqelem :: "[i,i,t]=>prop" ("(3_ =/ _ :/ _)" [10,10,10] 5) |
40 Eqelem :: "[i,i,t]=>prop" ("(3_ =/ _ :/ _)" [10,10,10] 5) |
41 Reduce :: "[i,i]=>prop" ("Reduce[_,_]") |
41 Reduce :: "[i,i]=>prop" ("Reduce[_,_]") |
42 (*Types*) |
42 (*Types*) |
43 "@PROD" :: "[id,t,t]=>t" ("(3PROD _:_./ _)" 10) |
43 "@PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10) |
44 "@SUM" :: "[id,t,t]=>t" ("(3SUM _:_./ _)" 10) |
44 "@SUM" :: "[idt,t,t]=>t" ("(3SUM _:_./ _)" 10) |
45 "+" :: "[t,t]=>t" (infixr 40) |
45 "+" :: "[t,t]=>t" (infixr 40) |
46 (*Invisible infixes!*) |
46 (*Invisible infixes!*) |
47 "@-->" :: "[t,t]=>t" ("(_ -->/ _)" [31,30] 30) |
47 "@-->" :: "[t,t]=>t" ("(_ -->/ _)" [31,30] 30) |
48 "@*" :: "[t,t]=>t" ("(_ */ _)" [51,50] 50) |
48 "@*" :: "[t,t]=>t" ("(_ */ _)" [51,50] 50) |
49 (*Functions*) |
49 (*Functions*) |
54 (*Pairing*) |
54 (*Pairing*) |
55 pair :: "[i,i]=>i" ("(1<_,/_>)") |
55 pair :: "[i,i]=>i" ("(1<_,/_>)") |
56 |
56 |
57 translations |
57 translations |
58 "PROD x:A. B" => "Prod(A, %x. B)" |
58 "PROD x:A. B" => "Prod(A, %x. B)" |
|
59 "A --> B" => "Prod(A, _K(B))" |
59 "SUM x:A. B" => "Sum(A, %x. B)" |
60 "SUM x:A. B" => "Sum(A, %x. B)" |
|
61 "A * B" => "Sum(A, _K(B))" |
60 |
62 |
61 rules |
63 rules |
62 |
64 |
63 (*Reduction: a weaker notion than equality; a hack for simplification. |
65 (*Reduction: a weaker notion than equality; a hack for simplification. |
64 Reduce[a,b] means either that a=b:A for some A or else that "a" and "b" |
66 Reduce[a,b] means either that a=b:A for some A or else that "a" and "b" |
242 end |
244 end |
243 |
245 |
244 |
246 |
245 ML |
247 ML |
246 |
248 |
247 val parse_translation = |
|
248 [("@-->", ndependent_tr "Prod"), ("@*", ndependent_tr "Sum")]; |
|
249 |
|
250 val print_translation = |
249 val print_translation = |
251 [("Prod", dependent_tr' ("@PROD", "@-->")), |
250 [("Prod", dependent_tr' ("@PROD", "@-->")), |
252 ("Sum", dependent_tr' ("@SUM", "@*"))]; |
251 ("Sum", dependent_tr' ("@SUM", "@*"))]; |
253 |
252 |