summaryrefslogtreecommitdiff
path: root/tests/lean/PoloniusList.lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/lean/PoloniusList.lean4
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 09f41056..d1ed10d2 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -6,13 +6,13 @@ open Primitives
namespace polonius_list
/- [polonius_list::List]
- Source: 'src/polonius_list.rs', lines 3:0-3:16 -/
+ Source: 'tests/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]:
- Source: 'src/polonius_list.rs', lines 13:0-13:76 -/
+ Source: 'tests/src/polonius_list.rs', lines 13:0-13:76 -/
divergent def get_list_at_x
(ls : List U32) (x : U32) :
Result ((List U32) × (List U32 → Result (List U32)))