diff --git a/exercise-book/src/kani-linked-list.md b/exercise-book/src/kani-linked-list.md index 4d79065b..620334f3 100644 --- a/exercise-book/src/kani-linked-list.md +++ b/exercise-book/src/kani-linked-list.md @@ -396,15 +396,15 @@ mod proofs {

-Generating a list of random elements. +Generating a linked list of random elements. -You can make a list by making an array first using [`from_fn`](https://doc.rust-lang.org/std/array/fn.from_fn.html) function. +You can make a list by making an array first using `kani::any()`. Then you can pass the array to a [`from_iter`](https://doc.rust-lang.org/std/iter/trait.FromIterator.html#tymethod.from_iter) method. ```rust ignore const TOTAL: usize = 10; -let items: [u32; TOTAL] = std::array::from_fn(|_| kani::any::()); +let items: [u32; TOTAL] = kani::any(); let mut list = DoublyLinkedList::from_iter(items.iter().copied()); assert_eq!(list.len(), TOTAL); diff --git a/exercise-solutions/kani-linked-list/src/lib.rs b/exercise-solutions/kani-linked-list/src/lib.rs index f40d1712..ba2c9046 100644 --- a/exercise-solutions/kani-linked-list/src/lib.rs +++ b/exercise-solutions/kani-linked-list/src/lib.rs @@ -284,7 +284,7 @@ mod proofs { #[cfg_attr(not(rust_analyzer), kani::unwind(20))] fn remove_at() { const TOTAL: usize = 10; - let items: [u32; TOTAL] = std::array::from_fn(|_| kani::any::()); + let items: [u32; TOTAL] = kani::any(); let mut list = DoublyLinkedList::from_iter(items.iter().copied()); assert_eq!(list.len(), TOTAL);