| allocNode : [a] |
| . |
| Unit -> rec t {l : <Cons {data : a,rest : rec t}#|Nil Unit> take}; |
| createEmptyList : [a] |
| . |
| U8 -> rec t {l : <Cons {data : a,rest : rec t}#|Nil Unit>}; |
| createEmptyList a = let node = (allocNode[a] : Unit |
| -> rec t {l : <Cons {data : a |
| ,rest : rec t}# |
| |Nil Unit> take}) (Unit : Unit) : rec t {l : <Cons {data : a |
| ,rest : rec t}# |
| |Nil Unit> take} |
| in put node : rec t {l : <Cons {data : a,rest : rec t}# |
| |Nil Unit> take}.l := Nil (Unit : Unit) : <Cons {data : a |
| ,rest : rec t}# |
| |Nil Unit> |
| end : rec t {l : <Cons {data : a,rest : rec t}# |
| |Nil Unit>} |
| end : rec t {l : <Cons {data : a,rest : rec t}#|Nil Unit>}; |