25 Zip ::"'a Seq -> 'b Seq -> ('a * 'b) Seq" |
25 Zip ::"'a Seq -> 'b Seq -> ('a * 'b) Seq" |
26 Flat ::"('a Seq) seq -> 'a Seq" |
26 Flat ::"('a Seq) seq -> 'a Seq" |
27 |
27 |
28 Filter2 ::"('a => bool) => 'a Seq -> 'a Seq" |
28 Filter2 ::"('a => bool) => 'a Seq -> 'a Seq" |
29 |
29 |
|
30 abbreviation |
|
31 Consq_syn ("(_/>>_)" [66,65] 65) where |
|
32 "a>>s == Consq a$s" |
|
33 |
|
34 notation (xsymbols) |
|
35 Consq_syn ("(_\<leadsto>_)" [66,65] 65) |
|
36 |
|
37 |
|
38 (* list Enumeration *) |
30 syntax |
39 syntax |
31 |
|
32 "@Consq" ::"'a => 'a Seq => 'a Seq" ("(_/>>_)" [66,65] 65) |
|
33 (* list Enumeration *) |
|
34 "_totlist" :: "args => 'a Seq" ("[(_)!]") |
40 "_totlist" :: "args => 'a Seq" ("[(_)!]") |
35 "_partlist" :: "args => 'a Seq" ("[(_)?]") |
41 "_partlist" :: "args => 'a Seq" ("[(_)?]") |
36 |
|
37 |
|
38 syntax (xsymbols) |
|
39 "@Consq" ::"'a => 'a Seq => 'a Seq" ("(_\<leadsto>_)" [66,65] 65) |
|
40 |
|
41 |
|
42 translations |
42 translations |
43 "a>>s" == "Consq a$s" |
|
44 "[x, xs!]" == "x>>[xs!]" |
43 "[x, xs!]" == "x>>[xs!]" |
45 "[x!]" == "x>>nil" |
44 "[x!]" == "x>>CONST nil" |
46 "[x, xs?]" == "x>>[xs?]" |
45 "[x, xs?]" == "x>>[xs?]" |
47 "[x?]" == "x>>UU" |
46 "[x?]" == "x>>CONST UU" |
48 |
47 |
49 defs |
48 defs |
50 |
49 |
51 Consq_def: "Consq a == LAM s. Def a ## s" |
50 Consq_def: "Consq a == LAM s. Def a ## s" |
52 |
51 |