blob: d53351976d21ec1031cf396f783ca9e9a2e0a35a [file] [log] [blame] [edit]
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>};