| changeset 5102 | 8c782c25a11e |
| parent 4283 | 92707e24b62b |
| child 5976 | 44290b71a85f |
| 5101:52e7c75acfe6 | 5102:8c782c25a11e |
|---|---|
5 |
5 |
6 Partial, Finite and Infinite Sequences (lazy lists), modeled as domain. |
6 Partial, Finite and Infinite Sequences (lazy lists), modeled as domain. |
7 *) |
7 *) |
8 |
8 |
9 |
9 |
10 Seq = HOLCF + |
10 Seq = HOLCF + Inductive + |
11 |
11 |
12 domain 'a seq = nil | "##" (HD::'a) (lazy TL::'a seq) (infixr 65) |
12 domain 'a seq = nil | "##" (HD::'a) (lazy TL::'a seq) (infixr 65) |
13 |
13 |
14 |
14 |
15 consts |
15 consts |