equal
deleted
inserted
replaced
27 sfinite :: "'a seq set" |
27 sfinite :: "'a seq set" |
28 Partial ::"'a seq => bool" |
28 Partial ::"'a seq => bool" |
29 Infinite ::"'a seq => bool" |
29 Infinite ::"'a seq => bool" |
30 |
30 |
31 nproj :: "nat => 'a seq => 'a" |
31 nproj :: "nat => 'a seq => 'a" |
|
32 sproj :: "nat => 'a seq => 'a seq" |
32 |
33 |
33 syntax |
34 syntax |
34 "@@" :: "'a seq => 'a seq => 'a seq" (infixr 65) |
35 "@@" :: "'a seq => 'a seq => 'a seq" (infixr 65) |
35 "Finite" :: "'a seq => bool" |
36 "Finite" :: "'a seq => bool" |
36 |
37 |
101 "szip == (fix`(LAM h t1 t2. case t1 of |
102 "szip == (fix`(LAM h t1 t2. case t1 of |
102 nil => nil |
103 nil => nil |
103 | x##xs => (case t2 of |
104 | x##xs => (case t2 of |
104 nil => UU |
105 nil => UU |
105 | y##ys => <x,y>##(h`xs`ys))))" |
106 | y##ys => <x,y>##(h`xs`ys))))" |
|
107 |
|
108 |
|
109 nproj_def |
|
110 "nproj == (%n tr.HD`(iterate n TL tr))" |
106 |
111 |
107 |
112 |
108 proj_def |
113 sproj_def |
109 "nproj == (%n tr. HD`(iterate n TL tr))" |
114 "sproj == (%n tr.iterate n TL tr)" |
|
115 |
|
116 |
110 |
117 |
111 Partial_def |
118 Partial_def |
112 "Partial x == (seq_finite x) & ~(Finite x)" |
119 "Partial x == (seq_finite x) & ~(Finite x)" |
113 |
120 |
114 Infinite_def |
121 Infinite_def |