| alloc : Unit -> rec t {l : <Cons {d : U8,r : rec t}#|End Unit> take}; |
| makeEmptyList : Unit -> rec t {l : <Cons {d : U8,r : rec t}#|End Unit>}; |
| makeEmptyList a = let r = (alloc[] : Unit |
| -> rec t {l : <Cons {d : U8,r : rec t}# |
| |End Unit> take}) (Unit : Unit) : rec t {l : <Cons {d : U8 |
| ,r : rec t}# |
| |End Unit> take} |
| in put r : rec t {l : <Cons {d : U8,r : rec t}# |
| |End Unit> take}.l := End (Unit : Unit) : <Cons {d : U8 |
| ,r : rec t}# |
| |End Unit> |
| end : rec t {l : <Cons {d : U8,r : rec t}#|End Unit>} |
| end : rec t {l : <Cons {d : U8,r : rec t}#|End Unit>}; |