38 "_update" :: "[ident, 'a] => update" ("(2_ :=/ _)") |
38 "_update" :: "[ident, 'a] => update" ("(2_ :=/ _)") |
39 "" :: "update => updates" ("_") |
39 "" :: "update => updates" ("_") |
40 "_updates" :: "[update, updates] => updates" ("_,/ _") |
40 "_updates" :: "[update, updates] => updates" ("_,/ _") |
41 "_record_update" :: "['a, updates] => 'b" ("_/(3'(| _ |'))" [900,0] 900) |
41 "_record_update" :: "['a, updates] => 'b" ("_/(3'(| _ |'))" [900,0] 900) |
42 |
42 |
43 syntax (input) (* FIXME (xsymbols) *) |
43 syntax (xsymbols) |
44 "_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)") |
44 "_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)") |
45 "_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)") |
45 "_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)") |
46 "_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
46 "_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
47 "_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)") |
47 "_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)") |
48 "_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900) |
48 "_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900) |