minigent/examples/6_recursive/06-list-push/expected.out

allocNode : [a]
            .
            Unit -> rec t {l : <Cons {data : a,rest : rec t}#|Nil Unit> take};
push : [a]
       .
       {data : a,list : rec t {l : <Cons {data : a,rest : rec t}#|Nil Unit>}}#
       -> rec t {l : <Cons {data : a,rest : rec t}#|Nil Unit>};
push r = 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 take r2 { data = x } = r : {data : a
                                       ,list : rec t {l : <Cons {data : a
                                                                ,rest : rec t}#
                                                          |Nil Unit>}}#
            in take r3 { list = y } = r2 : {data : a take,list : rec t}#
               in put node : rec t {l : <Cons {data : a,rest : rec t}#
                                        |Nil Unit> take}.l := Cons ({data = x : a
                                                                    ,rest = y : rec t} : {data : a
                                                                                         ,rest : rec t}#) : <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>}
            end : rec t {l : <Cons {data : a,rest : rec t}#|Nil Unit>}
         end : rec t {l : <Cons {data : a,rest : rec t}#|Nil Unit>};