163         // INVARIANT: Pin-init initializers can't be used on an existing `Arc`, so this value will  in new()
220         // INVARIANT: Pin-init initializers can't be used on an existing `Arc`, so this value will  in new()
265             // INVARIANT: A linked list with one item should be cyclic.  in push_back()
272             // SAFETY: By the type invariant, this pointer is valid or null. We just checked that  in push_back()
277             // INVARIANT: This correctly inserts `item` between `prev` and `next`.  in push_back()
304             // INVARIANT: A linked list with one item should be cyclic.  in push_front()
315             // INVARIANT: This correctly inserts `item` between `prev` and `next`.  in push_front()
420         // INVARIANT: There are three cases:  in remove_internal_inner()
431         // INVARIANT: `item` is being removed, so the pointers should be null.  in remove_internal_inner()
436         // INVARIANT: There are three cases:  in remove_internal_inner()
467             // INVARIANT: All of the elements in `other` become elements of `self`.  in push_all_back()
478             // INVARIANT: This correctly sets the pointers to merge both lists. We do not need to  in push_all_back()
488         // INVARIANT: The other list is now empty, so update its pointer.  in push_all_back()
508         // INVARIANT: If the list is empty, both pointers are null. Otherwise, both pointers point  in iter()
559         // INVARIANT: If `current` was the last element of the list, then this updates it to null.  in next()
615             // INVARIANT: Since `self.current` is in the `list`, its `next` pointer is also in the  in next()
632             // INVARIANT: Since `self.current` is in the `list`, its `prev` pointer is also in the  in prev()