Lines Matching full:invariant

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