| changeset 16417 | 9bc16273c2d4 |
| parent 13339 | 0f89104dd377 |
| child 24893 | b8ef7afe3a6b |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
12 STILL NEEDS: |
12 STILL NEEDS: |
13 co_recursion for defining lconst, flip, etc. |
13 co_recursion for defining lconst, flip, etc. |
14 a typing rule for it, based on some notion of "productivity..." |
14 a typing rule for it, based on some notion of "productivity..." |
15 *) |
15 *) |
16 |
16 |
17 theory LList = Main: |
17 theory LList imports Main begin |
18 |
18 |
19 consts |
19 consts |
20 llist :: "i=>i"; |
20 llist :: "i=>i"; |
21 |
21 |
22 codatatype |
22 codatatype |