Skip to content

Commit

Permalink
queue example working!
Browse files Browse the repository at this point in the history
  • Loading branch information
Benjamin Pierce committed Jun 9, 2024
1 parent 88a3bf7 commit 6a7d36c
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions src/examples/queue.broken.c
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,7 @@ predicate (datatype seq) IntQueueAux (pointer h, pointer t, i32 lastVal) {
return (Seq_Cons{head: lastVal, tail: Seq_Nil{}});
} else {
take C = Owned<struct int_queueCell>(h);
assert (!is_null(C.next)); // HERE IS THE KEY!
take TL = IntQueueAux(C.next, t, lastVal);
return (Seq_Cons { head: C.first, tail: TL });
}
Expand Down

0 comments on commit 6a7d36c

Please sign in to comment.