Merge branch 'main' into afromher/recursive_projectors

1 files changed, 29 insertions, 0 deletions

diff --git a/tests/src/polonius_list.rs b/tests/src/polonius_list.rs
new file mode 100644
index 00000000..a8d51e40
--- /dev/null
+++ b/tests/src/polonius_list.rs
@@ -0,0 +1,29 @@
+//@ charon-args=--polonius
+//@ aeneas-args=-test-trans-units
+#![allow(dead_code)]
+
+pub enum List<T> {
+    Cons(T, Box<List<T>>),
+    Nil,
+}
+
+/// An example which comes from the b-epsilon tree.
+///
+/// Returns a mutable borrow to the first portion of the list where we
+/// can find [x]. This allows to do in-place modifications (insertion, filtering)
+/// in a natural manner (this piece of code was inspired by the C++ BeTree).
+pub fn get_list_at_x<'a>(ls: &'a mut List<u32>, x: u32) -> &'a mut List<u32> {
+    match ls {
+        List::Nil => {
+            // We reached the end: just return it
+            ls
+        }
+        List::Cons(hd, tl) => {
+            if *hd == x {
+                ls // Doing this requires NLL
+            } else {
+                get_list_at_x(tl, x)
+            }
+        }
+    }
+}