From 137cc7335e64fcb70c254e7fd2a6fa353fb43e61 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 14:57:38 +0100
Subject: Regenerate the files

---
 tests/lean/PoloniusList.lean | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'tests/lean/PoloniusList.lean')

diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 07f206a8..0ef71791 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -5,12 +5,14 @@ open Primitives
 
 namespace polonius_list
 
-/- [polonius_list::List] -/
+/- [polonius_list::List]
+   Source: 'src/polonius_list.rs', lines 3:0-3:16 -/
 inductive List (T : Type) :=
 | Cons : T → List T → List T
 | Nil : List T
 
-/- [polonius_list::get_list_at_x]: forward function -/
+/- [polonius_list::get_list_at_x]: forward function
+   Source: 'src/polonius_list.rs', lines 13:0-13:76 -/
 divergent def get_list_at_x (ls : List U32) (x : U32) : Result (List U32) :=
   match ls with
   | List.Cons hd tl =>
@@ -19,7 +21,8 @@ divergent def get_list_at_x (ls : List U32) (x : U32) : Result (List U32) :=
     else get_list_at_x tl x
   | List.Nil => Result.ret List.Nil
 
-/- [polonius_list::get_list_at_x]: backward function 0 -/
+/- [polonius_list::get_list_at_x]: backward function 0
+   Source: 'src/polonius_list.rs', lines 13:0-13:76 -/
 divergent def get_list_at_x_back
   (ls : List U32) (x : U32) (ret0 : List U32) : Result (List U32) :=
   match ls with
-- 
cgit v1.2.3