summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/lean/BetreeMain/Funs.lean12
-rw-r--r--tests/lean/BetreeMain/FunsExternal_Template.lean3
-rw-r--r--tests/lean/Demo/Demo.lean32
-rw-r--r--tests/lean/External/Funs.lean4
-rw-r--r--tests/lean/External/FunsExternal_Template.lean9
-rw-r--r--tests/lean/External/TypesExternal_Template.lean3
-rw-r--r--tests/lean/Hashmap/Funs.lean28
-rw-r--r--tests/lean/HashmapMain/Funs.lean28
-rw-r--r--tests/lean/Loops.lean80
-rw-r--r--tests/lean/NoNestedBorrows.lean16
-rw-r--r--tests/lean/Paper.lean16
-rw-r--r--tests/lean/PoloniusList.lean4
-rw-r--r--tests/lean/Traits.lean3
13 files changed, 121 insertions, 117 deletions
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index ca9b48da..2fbcd6a4 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -192,12 +192,12 @@ divergent def betree.Node.lookup_first_message_for_key
do
let (l, lookup_first_message_for_key_back) ←
betree.Node.lookup_first_message_for_key key next_msgs
- let back_'a :=
+ let back :=
fun ret =>
do
let next_msgs1 ← lookup_first_message_for_key_back ret
Result.ret (betree.List.Cons (i, m) next_msgs1)
- Result.ret (l, back_'a)
+ Result.ret (l, back)
| betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]:
@@ -364,12 +364,12 @@ divergent def betree.Node.lookup_first_message_after_key
do
let (l, lookup_first_message_after_key_back) ←
betree.Node.lookup_first_message_after_key key next_msgs
- let back_'a :=
+ let back :=
fun ret =>
do
let next_msgs1 ← lookup_first_message_after_key_back ret
Result.ret (betree.List.Cons (k, m) next_msgs1)
- Result.ret (l, back_'a)
+ Result.ret (l, back)
else Result.ret (betree.List.Cons (k, m) next_msgs, Result.ret)
| betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
@@ -468,12 +468,12 @@ divergent def betree.Node.lookup_mut_in_bindings
do
let (l, lookup_mut_in_bindings_back) ←
betree.Node.lookup_mut_in_bindings key tl
- let back_'a :=
+ let back :=
fun ret =>
do
let tl1 ← lookup_mut_in_bindings_back ret
Result.ret (betree.List.Cons (i, i1) tl1)
- Result.ret (l, back_'a)
+ Result.ret (l, back)
| betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]:
diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/BetreeMain/FunsExternal_Template.lean
index eaa4b6c2..0b3e4ef4 100644
--- a/tests/lean/BetreeMain/FunsExternal_Template.lean
+++ b/tests/lean/BetreeMain/FunsExternal_Template.lean
@@ -29,7 +29,8 @@ axiom betree_utils.store_leaf_node
: U64 → betree.List (U64 × U64) → State → Result (State × Unit)
/- [core::option::{core::option::Option<T>}::unwrap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 -/
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+ Name pattern: core::option::{core::option::Option<@T>}::unwrap -/
axiom core.option.Option.unwrap
(T : Type) : Option T → State → Result (State × T)
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 4acc69c8..6d9fef8e 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -12,10 +12,10 @@ def choose
Result (T × (T → Result (T × T)))
:=
if b
- then let back_'a := fun ret => Result.ret (ret, y)
- Result.ret (x, back_'a)
- else let back_'a := fun ret => Result.ret (x, ret)
- Result.ret (y, back_'a)
+ then let back := fun ret => Result.ret (ret, y)
+ Result.ret (x, back)
+ else let back := fun ret => Result.ret (x, ret)
+ Result.ret (y, back)
/- [demo::mul2_add1]:
Source: 'src/demo.rs', lines 13:0-13:31 -/
@@ -73,18 +73,18 @@ divergent def list_nth_mut
| CList.CCons x tl =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (CList.CCons ret tl)
- Result.ret (x, back_'a)
+ let back := fun ret => Result.ret (CList.CCons ret tl)
+ Result.ret (x, back)
else
do
let i1 ← i - 1#u32
let (t, list_nth_mut_back) ← list_nth_mut T tl i1
- let back_'a :=
+ let back :=
fun ret =>
do
let tl1 ← list_nth_mut_back ret
Result.ret (CList.CCons x tl1)
- Result.ret (t, back_'a)
+ Result.ret (t, back)
| CList.CNil => Result.fail .panic
/- [demo::list_nth_mut1]: loop 0:
@@ -97,17 +97,17 @@ divergent def list_nth_mut1_loop
| CList.CCons x tl =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (CList.CCons ret tl)
- Result.ret (x, back_'a)
+ let back := fun ret => Result.ret (CList.CCons ret tl)
+ Result.ret (x, back)
else
do
let i1 ← i - 1#u32
- let (t, back_'a) ← list_nth_mut1_loop T tl i1
- let back_'a1 :=
+ let (t, back) ← list_nth_mut1_loop T tl i1
+ let back1 :=
fun ret => do
- let tl1 ← back_'a ret
+ let tl1 ← back ret
Result.ret (CList.CCons x tl1)
- Result.ret (t, back_'a1)
+ Result.ret (t, back1)
| CList.CNil => Result.fail .panic
/- [demo::list_nth_mut1]:
@@ -138,12 +138,12 @@ divergent def list_tail
| CList.CCons t tl =>
do
let (c, list_tail_back) ← list_tail T tl
- let back_'a :=
+ let back :=
fun ret =>
do
let tl1 ← list_tail_back ret
Result.ret (CList.CCons t tl1)
- Result.ret (c, back_'a)
+ Result.ret (c, back)
| CList.CNil => Result.ret (CList.CNil, Result.ret)
/- Trait declaration: [demo::Counter]
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 8b645037..cfb2cb3c 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -39,8 +39,8 @@ def custom_swap
:=
do
let (st1, (x1, y1)) ← core.mem.swap T x y st
- let back_'a := fun ret st2 => Result.ret (st2, (ret, y1))
- Result.ret (st1, (x1, back_'a))
+ let back := fun ret st2 => Result.ret (st2, (ret, y1))
+ Result.ret (st1, (x1, back))
/- [external::test_custom_swap]:
Source: 'src/external.rs', lines 29:0-29:59 -/
diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean
index 7e237369..38151dc9 100644
--- a/tests/lean/External/FunsExternal_Template.lean
+++ b/tests/lean/External/FunsExternal_Template.lean
@@ -7,17 +7,20 @@ open Primitives
open external
/- [core::mem::swap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 -/
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
+ Name pattern: core::mem::swap -/
axiom core.mem.swap
(T : Type) : T → T → State → Result (State × (T × T))
/- [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 -/
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
+ Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new -/
axiom core.num.nonzero.NonZeroU32.new
: U32 → State → Result (State × (Option core.num.nonzero.NonZeroU32))
/- [core::option::{core::option::Option<T>}::unwrap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 -/
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+ Name pattern: core::option::{core::option::Option<@T>}::unwrap -/
axiom core.option.Option.unwrap
(T : Type) : Option T → State → Result (State × T)
diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean
index 85fef236..84245531 100644
--- a/tests/lean/External/TypesExternal_Template.lean
+++ b/tests/lean/External/TypesExternal_Template.lean
@@ -5,7 +5,8 @@ import Base
open Primitives
/- [core::num::nonzero::NonZeroU32]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
+ Name pattern: core::num::nonzero::NonZeroU32 -/
axiom core.num.nonzero.NonZeroU32 : Type
/- The state type used in the state-error monad -/
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 1c95f7c9..363d751a 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -79,8 +79,8 @@ divergent def HashMap.clear_loop
Source: 'src/hashmap.rs', lines 80:4-80:27 -/
def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) :=
do
- let back ← HashMap.clear_loop T self.slots 0#usize
- Result.ret { self with num_entries := 0#usize, slots := back }
+ let hm ← HashMap.clear_loop T self.slots 0#usize
+ Result.ret { self with num_entries := 0#usize, slots := hm }
/- [hashmap::{hashmap::HashMap<T>}::len]:
Source: 'src/hashmap.rs', lines 90:4-90:30 -/
@@ -99,8 +99,8 @@ divergent def HashMap.insert_in_list_loop
then Result.ret (false, List.Cons ckey value tl)
else
do
- let (b, back) ← HashMap.insert_in_list_loop T key value tl
- Result.ret (b, List.Cons ckey cvalue back)
+ let (b, tl1) ← HashMap.insert_in_list_loop T key value tl
+ Result.ret (b, List.Cons ckey cvalue tl1)
| List.Nil => Result.ret (true, List.Cons key value List.Nil)
/- [hashmap::{hashmap::HashMap<T>}::insert_in_list]:
@@ -287,17 +287,17 @@ divergent def HashMap.get_mut_in_list_loop
| List.Cons ckey cvalue tl =>
if ckey = key
then
- let back_'a := fun ret => Result.ret (List.Cons ckey ret tl)
- Result.ret (cvalue, back_'a)
+ let back := fun ret => Result.ret (List.Cons ckey ret tl)
+ Result.ret (cvalue, back)
else
do
- let (t, back_'a) ← HashMap.get_mut_in_list_loop T tl key
- let back_'a1 :=
+ let (t, back) ← HashMap.get_mut_in_list_loop T tl key
+ let back1 :=
fun ret =>
do
- let tl1 ← back_'a ret
+ let tl1 ← back ret
Result.ret (List.Cons ckey cvalue tl1)
- Result.ret (t, back_'a1)
+ Result.ret (t, back1)
| List.Nil => Result.fail .panic
/- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]:
@@ -322,13 +322,13 @@ def HashMap.get_mut
alloc.vec.Vec.index_mut (List T) Usize
(core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots hash_mod
let (t, get_mut_in_list_back) ← HashMap.get_mut_in_list T l key
- let back_'a :=
+ let back :=
fun ret =>
do
let l1 ← get_mut_in_list_back ret
let v ← index_mut_back l1
Result.ret { self with slots := v }
- Result.ret (t, back_'a)
+ Result.ret (t, back)
/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
Source: 'src/hashmap.rs', lines 265:4-291:5 -/
@@ -345,8 +345,8 @@ divergent def HashMap.remove_from_list_loop
| List.Nil => Result.fail .panic
else
do
- let (o, back) ← HashMap.remove_from_list_loop T key tl
- Result.ret (o, List.Cons ckey t back)
+ let (o, tl1) ← HashMap.remove_from_list_loop T key tl
+ Result.ret (o, List.Cons ckey t tl1)
| List.Nil => Result.ret (none, List.Nil)
/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]:
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index 6a6934b8..6fac6940 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -83,8 +83,8 @@ divergent def hashmap.HashMap.clear_loop
def hashmap.HashMap.clear
(T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
do
- let back ← hashmap.HashMap.clear_loop T self.slots 0#usize
- Result.ret { self with num_entries := 0#usize, slots := back }
+ let hm ← hashmap.HashMap.clear_loop T self.slots 0#usize
+ Result.ret { self with num_entries := 0#usize, slots := hm }
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]:
Source: 'src/hashmap.rs', lines 90:4-90:30 -/
@@ -103,8 +103,8 @@ divergent def hashmap.HashMap.insert_in_list_loop
then Result.ret (false, hashmap.List.Cons ckey value tl)
else
do
- let (b, back) ← hashmap.HashMap.insert_in_list_loop T key value tl
- Result.ret (b, hashmap.List.Cons ckey cvalue back)
+ let (b, tl1) ← hashmap.HashMap.insert_in_list_loop T key value tl
+ Result.ret (b, hashmap.List.Cons ckey cvalue tl1)
| hashmap.List.Nil =>
Result.ret (true, hashmap.List.Cons key value hashmap.List.Nil)
@@ -302,17 +302,17 @@ divergent def hashmap.HashMap.get_mut_in_list_loop
| hashmap.List.Cons ckey cvalue tl =>
if ckey = key
then
- let back_'a := fun ret => Result.ret (hashmap.List.Cons ckey ret tl)
- Result.ret (cvalue, back_'a)
+ let back := fun ret => Result.ret (hashmap.List.Cons ckey ret tl)
+ Result.ret (cvalue, back)
else
do
- let (t, back_'a) ← hashmap.HashMap.get_mut_in_list_loop T tl key
- let back_'a1 :=
+ let (t, back) ← hashmap.HashMap.get_mut_in_list_loop T tl key
+ let back1 :=
fun ret =>
do
- let tl1 ← back_'a ret
+ let tl1 ← back ret
Result.ret (hashmap.List.Cons ckey cvalue tl1)
- Result.ret (t, back_'a1)
+ Result.ret (t, back1)
| hashmap.List.Nil => Result.fail .panic
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]:
@@ -338,13 +338,13 @@ def hashmap.HashMap.get_mut
(core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots
hash_mod
let (t, get_mut_in_list_back) ← hashmap.HashMap.get_mut_in_list T l key
- let back_'a :=
+ let back :=
fun ret =>
do
let l1 ← get_mut_in_list_back ret
let v ← index_mut_back l1
Result.ret { self with slots := v }
- Result.ret (t, back_'a)
+ Result.ret (t, back)
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
Source: 'src/hashmap.rs', lines 265:4-291:5 -/
@@ -364,8 +364,8 @@ divergent def hashmap.HashMap.remove_from_list_loop
| hashmap.List.Nil => Result.fail .panic
else
do
- let (o, back) ← hashmap.HashMap.remove_from_list_loop T key tl
- Result.ret (o, hashmap.List.Cons ckey t back)
+ let (o, tl1) ← hashmap.HashMap.remove_from_list_loop T key tl
+ Result.ret (o, hashmap.List.Cons ckey t tl1)
| hashmap.List.Nil => Result.ret (none, hashmap.List.Nil)
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]:
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 0f3d77c2..27434db8 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -295,22 +295,22 @@ divergent def list_nth_mut_loop_pair_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (List.Cons ret tl0)
- let back_'b := fun ret => Result.ret (List.Cons ret tl1)
- Result.ret ((x0, x1), back_'a, back_'b)
+ let back'a := fun ret => Result.ret (List.Cons ret tl0)
+ let back'b := fun ret => Result.ret (List.Cons ret tl1)
+ Result.ret ((x0, x1), back'a, back'b)
else
do
let i1 ← i - 1#u32
- let (p, back_'a, back_'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1
- let back_'a1 :=
+ let (p, back'a, back'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1
+ let back'a1 :=
fun ret => do
- let tl01 ← back_'a ret
+ let tl01 ← back'a ret
Result.ret (List.Cons x0 tl01)
- let back_'b1 :=
+ let back'b1 :=
fun ret => do
- let tl11 ← back_'b ret
+ let tl11 ← back'b ret
Result.ret (List.Cons x1 tl11)
- Result.ret (p, back_'a1, back_'b1)
+ Result.ret (p, back'a1, back'b1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -356,21 +356,21 @@ divergent def list_nth_mut_loop_pair_merge_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back_'a :=
+ let back :=
fun ret =>
let (t, t1) := ret
Result.ret (List.Cons t tl0, List.Cons t1 tl1)
- Result.ret ((x0, x1), back_'a)
+ Result.ret ((x0, x1), back)
else
do
let i1 ← i - 1#u32
- let (p, back_'a) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1
- let back_'a1 :=
+ let (p, back) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1
+ let back1 :=
fun ret =>
do
- let (tl01, tl11) ← back_'a ret
+ let (tl01, tl11) ← back ret
Result.ret (List.Cons x0 tl01, List.Cons x1 tl11)
- Result.ret (p, back_'a1)
+ Result.ret (p, back1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -417,17 +417,17 @@ divergent def list_nth_mut_shared_loop_pair_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (List.Cons ret tl0)
- Result.ret ((x0, x1), back_'a)
+ let back := fun ret => Result.ret (List.Cons ret tl0)
+ Result.ret ((x0, x1), back)
else
do
let i1 ← i - 1#u32
- let (p, back_'a) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1
- let back_'a1 :=
+ let (p, back) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1
+ let back1 :=
fun ret => do
- let tl01 ← back_'a ret
+ let tl01 ← back ret
Result.ret (List.Cons x0 tl01)
- Result.ret (p, back_'a1)
+ Result.ret (p, back1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -451,18 +451,17 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (List.Cons ret tl0)
- Result.ret ((x0, x1), back_'a)
+ let back := fun ret => Result.ret (List.Cons ret tl0)
+ Result.ret ((x0, x1), back)
else
do
let i1 ← i - 1#u32
- let (p, back_'a) ←
- list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1
- let back_'a1 :=
+ let (p, back) ← list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1
+ let back1 :=
fun ret => do
- let tl01 ← back_'a ret
+ let tl01 ← back ret
Result.ret (List.Cons x0 tl01)
- Result.ret (p, back_'a1)
+ Result.ret (p, back1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -486,17 +485,17 @@ divergent def list_nth_shared_mut_loop_pair_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back_'b := fun ret => Result.ret (List.Cons ret tl1)
- Result.ret ((x0, x1), back_'b)
+ let back := fun ret => Result.ret (List.Cons ret tl1)
+ Result.ret ((x0, x1), back)
else
do
let i1 ← i - 1#u32
- let (p, back_'b) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1
- let back_'b1 :=
+ let (p, back) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1
+ let back1 :=
fun ret => do
- let tl11 ← back_'b ret
+ let tl11 ← back ret
Result.ret (List.Cons x1 tl11)
- Result.ret (p, back_'b1)
+ Result.ret (p, back1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -520,18 +519,17 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (List.Cons ret tl1)
- Result.ret ((x0, x1), back_'a)
+ let back := fun ret => Result.ret (List.Cons ret tl1)
+ Result.ret ((x0, x1), back)
else
do
let i1 ← i - 1#u32
- let (p, back_'a) ←
- list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1
- let back_'a1 :=
+ let (p, back) ← list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1
+ let back1 :=
fun ret => do
- let tl11 ← back_'a ret
+ let tl11 ← back ret
Result.ret (List.Cons x1 tl11)
- Result.ret (p, back_'a1)
+ Result.ret (p, back1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 5f9ec0f2..b90f6aef 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -331,10 +331,10 @@ def choose
Result (T × (T → Result (T × T)))
:=
if b
- then let back_'a := fun ret => Result.ret (ret, y)
- Result.ret (x, back_'a)
- else let back_'a := fun ret => Result.ret (x, ret)
- Result.ret (y, back_'a)
+ then let back := fun ret => Result.ret (ret, y)
+ Result.ret (x, back)
+ else let back := fun ret => Result.ret (x, ret)
+ Result.ret (y, back)
/- [no_nested_borrows::choose_test]:
Source: 'src/no_nested_borrows.rs', lines 282:0-282:20 -/
@@ -406,18 +406,18 @@ divergent def list_nth_mut
| List.Cons x tl =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (List.Cons ret tl)
- Result.ret (x, back_'a)
+ let back := fun ret => Result.ret (List.Cons ret tl)
+ Result.ret (x, back)
else
do
let i1 ← i - 1#u32
let (t, list_nth_mut_back) ← list_nth_mut T tl i1
- let back_'a :=
+ let back :=
fun ret =>
do
let tl1 ← list_nth_mut_back ret
Result.ret (List.Cons x tl1)
- Result.ret (t, back_'a)
+ Result.ret (t, back)
| List.Nil => Result.fail .panic
/- [no_nested_borrows::list_rev_aux]:
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 924ff36c..5b00aa83 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -29,10 +29,10 @@ def choose
Result (T × (T → Result (T × T)))
:=
if b
- then let back_'a := fun ret => Result.ret (ret, y)
- Result.ret (x, back_'a)
- else let back_'a := fun ret => Result.ret (x, ret)
- Result.ret (y, back_'a)
+ then let back := fun ret => Result.ret (ret, y)
+ Result.ret (x, back)
+ else let back := fun ret => Result.ret (x, ret)
+ Result.ret (y, back)
/- [paper::test_choose]:
Source: 'src/paper.rs', lines 23:0-23:20 -/
@@ -68,18 +68,18 @@ divergent def list_nth_mut
| List.Cons x tl =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (List.Cons ret tl)
- Result.ret (x, back_'a)
+ let back := fun ret => Result.ret (List.Cons ret tl)
+ Result.ret (x, back)
else
do
let i1 ← i - 1#u32
let (t, list_nth_mut_back) ← list_nth_mut T tl i1
- let back_'a :=
+ let back :=
fun ret =>
do
let tl1 ← list_nth_mut_back ret
Result.ret (List.Cons x tl1)
- Result.ret (t, back_'a)
+ Result.ret (t, back)
| List.Nil => Result.fail .panic
/- [paper::sum]:
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 59c557a0..c657237f 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -24,12 +24,12 @@ divergent def get_list_at_x
else
do
let (l, get_list_at_x_back) ← get_list_at_x tl x
- let back_'a :=
+ let back :=
fun ret =>
do
let tl1 ← get_list_at_x_back ret
Result.ret (List.Cons hd tl1)
- Result.ret (l, back_'a)
+ Result.ret (l, back)
| List.Nil => Result.ret (List.Nil, Result.ret)
end polonius_list
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index acddd1a9..766b109d 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -512,7 +512,8 @@ structure Foo (T U : Type) where
y : U
/- [core::result::Result]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 -/
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21
+ Name pattern: core::result::Result -/
inductive core.result.Result (T E : Type) :=
| Ok : T → core.result.Result T E
| Err : E → core.result.Result T E
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 14:54:04 +0000