summaryrefslogtreecommitdiff
path: root/tests/lean/PoloniusList.lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/PoloniusList.lean')
-rw-r--r--tests/lean/PoloniusList.lean9
1 files changed, 6 insertions, 3 deletions
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