equal
deleted
inserted
replaced
33 "@*" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55) |
33 "@*" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55) |
34 "@Subtype" :: "[idt, 'a set, o] => 'a set" ("(1{_: _ ./ _})") |
34 "@Subtype" :: "[idt, 'a set, o] => 'a set" ("(1{_: _ ./ _})") |
35 |
35 |
36 translations |
36 translations |
37 "PROD x:A. B" => "Pi(A, %x. B)" |
37 "PROD x:A. B" => "Pi(A, %x. B)" |
|
38 "A -> B" => "Pi(A, _K(B))" |
38 "SUM x:A. B" => "Sigma(A, %x. B)" |
39 "SUM x:A. B" => "Sigma(A, %x. B)" |
|
40 "A * B" => "Sigma(A, _K(B))" |
39 "{x: A. B}" == "Subtype(A, %x. B)" |
41 "{x: A. B}" == "Subtype(A, %x. B)" |
40 |
42 |
41 rules |
43 rules |
42 |
44 |
43 Subtype_def "{x:A.P(x)} == {x.x:A & P(x)}" |
45 Subtype_def "{x:A.P(x)} == {x.x:A & P(x)}" |
61 end |
63 end |
62 |
64 |
63 |
65 |
64 ML |
66 ML |
65 |
67 |
66 val parse_translation = |
|
67 [("@->", ndependent_tr "Pi"), |
|
68 ("@*", ndependent_tr "Sigma")]; |
|
69 |
|
70 val print_translation = |
68 val print_translation = |
71 [("Pi", dependent_tr' ("@Pi", "@->")), |
69 [("Pi", dependent_tr' ("@Pi", "@->")), |
72 ("Sigma", dependent_tr' ("@Sigma", "@*"))]; |
70 ("Sigma", dependent_tr' ("@Sigma", "@*"))]; |
73 |
71 |