| changeset 2278 | d63ffafce255 |
| parent 1479 | 21eb5e156d91 |
| child 2291 | fbd14a05fb88 |
| 2277:9174de6c7143 | 2278:d63ffafce255 |
|---|---|
41 rules |
41 rules |
42 |
42 |
43 lub "lub(S) = (@x. S <<| x)" |
43 lub "lub(S) = (@x. S <<| x)" |
44 |
44 |
45 (* start 8bit 1 *) |
45 (* start 8bit 1 *) |
46 |
|
47 syntax |
|
48 "Glub" :: "[pttrn, 'a] => 'a" ("(3×_./ _)" 10) |
|
49 |
|
50 translations |
|
51 "×x.t" == "lub(range(%x.t))" |
|
52 |
|
46 (* end 8bit 1 *) |
53 (* end 8bit 1 *) |
47 |
54 |
48 end |
55 end |
49 |
56 |
50 |
57 |