equal
deleted
inserted
replaced
53 "_pattern" :: [pttrn, patterns] => pttrn ("'(_,/_')") |
53 "_pattern" :: [pttrn, patterns] => pttrn ("'(_,/_')") |
54 "" :: pttrn => patterns ("_") |
54 "" :: pttrn => patterns ("_") |
55 "_patterns" :: [pttrn, patterns] => patterns ("_,/_") |
55 "_patterns" :: [pttrn, patterns] => patterns ("_,/_") |
56 |
56 |
57 "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10) |
57 "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10) |
58 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ Times _" [81, 80] 80) |
58 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" (infixr "<*>" 80) |
59 |
59 |
60 translations |
60 translations |
61 "(x, y, z)" == "(x, (y, z))" |
61 "(x, y, z)" == "(x, (y, z))" |
62 "(x, y)" == "Pair x y" |
62 "(x, y)" == "Pair x y" |
63 |
63 |
66 "_abs (Pair x y) t" => "%(x,y).t" |
66 "_abs (Pair x y) t" => "%(x,y).t" |
67 (* The last rule accommodates tuples in `case C ... (x,y) ... => ...' |
67 (* The last rule accommodates tuples in `case C ... (x,y) ... => ...' |
68 The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *) |
68 The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *) |
69 |
69 |
70 "SIGMA x:A. B" => "Sigma A (%x. B)" |
70 "SIGMA x:A. B" => "Sigma A (%x. B)" |
71 "A Times B" => "Sigma A (_K B)" |
71 "A <*> B" => "Sigma A (_K B)" |
72 |
72 |
73 syntax (symbols) |
73 syntax (symbols) |
74 "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\\<Sigma> _\\<in>_./ _)" 10) |
74 "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\\<Sigma> _\\<in>_./ _)" 10) |
75 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \\<times> _" [81, 80] 80) |
75 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \\<times> _" [81, 80] 80) |
76 |
76 |