From cd5542fc82edee11181a43e3a342a2567c929e7e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 14:53:12 +0200
Subject: Regenerate the tests

---
 tests/lean/NoNestedBorrows.lean | 138 ++++++++++++++++++++--------------------
 1 file changed, 69 insertions(+), 69 deletions(-)

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

diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index f0438050..01f6736c 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -62,7 +62,7 @@ def cast_bool_to_bool (x : Bool) : Result Bool :=
    Source: 'tests/src/no_nested_borrows.rs', lines 63:0-63:14 -/
 def test2 : Result Unit :=
   do
-  let _ ← 23#u32 + 44#u32
+  let _ ← 23u32 + 44u32
   Result.ok ()
 
 /- Unit test for [no_nested_borrows::test2] -/
@@ -79,10 +79,10 @@ def get_max (x : U32) (y : U32) : Result U32 :=
    Source: 'tests/src/no_nested_borrows.rs', lines 83:0-83:14 -/
 def test3 : Result Unit :=
   do
-  let x ← get_max 4#u32 3#u32
-  let y ← get_max 10#u32 11#u32
+  let x ← get_max 4u32 3u32
+  let y ← get_max 10u32 11u32
   let z ← x + y
-  if z = 15#u32
+  if z = 15u32
   then Result.ok ()
   else Result.fail .panic
 
@@ -93,8 +93,8 @@ def test3 : Result Unit :=
    Source: 'tests/src/no_nested_borrows.rs', lines 90:0-90:18 -/
 def test_neg1 : Result Unit :=
   do
-  let y ← -. 3#i32
-  if y = (-3)#i32
+  let y ← -. 3i32
+  if y = (-3)i32
   then Result.ok ()
   else Result.fail .panic
 
@@ -104,7 +104,7 @@ def test_neg1 : Result Unit :=
 /- [no_nested_borrows::refs_test1]:
    Source: 'tests/src/no_nested_borrows.rs', lines 97:0-97:19 -/
 def refs_test1 : Result Unit :=
-  if 1#i32 = 1#i32
+  if 1i32 = 1i32
   then Result.ok ()
   else Result.fail .panic
 
@@ -114,12 +114,12 @@ def refs_test1 : Result Unit :=
 /- [no_nested_borrows::refs_test2]:
    Source: 'tests/src/no_nested_borrows.rs', lines 108:0-108:19 -/
 def refs_test2 : Result Unit :=
-  if 2#i32 = 2#i32
+  if 2i32 = 2i32
   then
-    if 0#i32 = 0#i32
+    if 0i32 = 0i32
     then
-      if 2#i32 = 2#i32
-      then if 2#i32 = 2#i32
+      if 2i32 = 2i32
+      then if 2i32 = 2i32
            then Result.ok ()
            else Result.fail .panic
       else Result.fail .panic
@@ -141,10 +141,10 @@ def test_list1 : Result Unit :=
    Source: 'tests/src/no_nested_borrows.rs', lines 129:0-129:18 -/
 def test_box1 : Result Unit :=
   do
-  let (_, deref_mut_back) ← alloc.boxed.Box.deref_mut I32 0#i32
-  let b ← deref_mut_back 1#i32
+  let (_, deref_mut_back) ← alloc.boxed.Box.deref_mut I32 0i32
+  let b ← deref_mut_back 1i32
   let x ← alloc.boxed.Box.deref I32 b
-  if x = 1#i32
+  if x = 1i32
   then Result.ok ()
   else Result.fail .panic
 
@@ -174,8 +174,8 @@ def test_panic (b : Bool) : Result Unit :=
    Source: 'tests/src/no_nested_borrows.rs', lines 160:0-160:22 -/
 def test_copy_int : Result Unit :=
   do
-  let y ← copy_int 0#i32
-  if 0#i32 = y
+  let y ← copy_int 0i32
+  if 0i32 = y
   then Result.ok ()
   else Result.fail .panic
 
@@ -193,7 +193,7 @@ def is_cons (T : Type) (l : List T) : Result Bool :=
    Source: 'tests/src/no_nested_borrows.rs', lines 174:0-174:21 -/
 def test_is_cons : Result Unit :=
   do
-  let b ← is_cons I32 (List.Cons 0#i32 List.Nil)
+  let b ← is_cons I32 (List.Cons 0i32 List.Nil)
   if b
   then Result.ok ()
   else Result.fail .panic
@@ -212,9 +212,9 @@ def split_list (T : Type) (l : List T) : Result (T × (List T)) :=
    Source: 'tests/src/no_nested_borrows.rs', lines 188:0-188:24 -/
 def test_split_list : Result Unit :=
   do
-  let p ← split_list I32 (List.Cons 0#i32 List.Nil)
+  let p ← split_list I32 (List.Cons 0i32 List.Nil)
   let (hd, _) := p
-  if hd = 0#i32
+  if hd = 0i32
   then Result.ok ()
   else Result.fail .panic
 
@@ -237,14 +237,14 @@ def choose
    Source: 'tests/src/no_nested_borrows.rs', lines 203:0-203:20 -/
 def choose_test : Result Unit :=
   do
-  let (z, choose_back) ← choose I32 true 0#i32 0#i32
-  let z1 ← z + 1#i32
-  if z1 = 1#i32
+  let (z, choose_back) ← choose I32 true 0i32 0i32
+  let z1 ← z + 1i32
+  if z1 = 1i32
   then
     do
     let (x, y) ← choose_back z1
-    if x = 1#i32
-    then if y = 0#i32
+    if x = 1i32
+    then if y = 0i32
          then Result.ok ()
          else Result.fail .panic
     else Result.fail .panic
@@ -285,18 +285,18 @@ divergent def list_length (T : Type) (l : List T) : Result U32 :=
   match l with
   | List.Cons _ l1 => do
                       let i ← list_length T l1
-                      1#u32 + i
-  | List.Nil => Result.ok 0#u32
+                      1u32 + i
+  | List.Nil => Result.ok 0u32
 
 /- [no_nested_borrows::list_nth_shared]:
    Source: 'tests/src/no_nested_borrows.rs', lines 273:0-273:62 -/
 divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T :=
   match l with
   | List.Cons x tl =>
-    if i = 0#u32
+    if i = 0u32
     then Result.ok x
     else do
-         let i1 ← i - 1#u32
+         let i1 ← i - 1u32
          list_nth_shared T tl i1
   | List.Nil => Result.fail .panic
 
@@ -306,13 +306,13 @@ divergent def list_nth_mut
   (T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) :=
   match l with
   | List.Cons x tl =>
-    if i = 0#u32
+    if i = 0u32
     then
       let back := fun ret => Result.ok (List.Cons ret tl)
       Result.ok (x, back)
     else
       do
-      let i1 ← i - 1#u32
+      let i1 ← i - 1u32
       let (t, list_nth_mut_back) ← list_nth_mut T tl i1
       let back :=
         fun ret =>
@@ -340,37 +340,37 @@ def list_rev (T : Type) (l : List T) : Result (List T) :=
    Source: 'tests/src/no_nested_borrows.rs', lines 324:0-324:28 -/
 def test_list_functions : Result Unit :=
   do
-  let l := List.Cons 2#i32 List.Nil
-  let l1 := List.Cons 1#i32 l
-  let i ← list_length I32 (List.Cons 0#i32 l1)
-  if i = 3#u32
+  let l := List.Cons 2i32 List.Nil
+  let l1 := List.Cons 1i32 l
+  let i ← list_length I32 (List.Cons 0i32 l1)
+  if i = 3u32
   then
     do
-    let i1 ← list_nth_shared I32 (List.Cons 0#i32 l1) 0#u32
-    if i1 = 0#i32
+    let i1 ← list_nth_shared I32 (List.Cons 0i32 l1) 0u32
+    if i1 = 0i32
     then
       do
-      let i2 ← list_nth_shared I32 (List.Cons 0#i32 l1) 1#u32
-      if i2 = 1#i32
+      let i2 ← list_nth_shared I32 (List.Cons 0i32 l1) 1u32
+      if i2 = 1i32
       then
         do
-        let i3 ← list_nth_shared I32 (List.Cons 0#i32 l1) 2#u32
-        if i3 = 2#i32
+        let i3 ← list_nth_shared I32 (List.Cons 0i32 l1) 2u32
+        if i3 = 2i32
         then
           do
           let (_, list_nth_mut_back) ←
-            list_nth_mut I32 (List.Cons 0#i32 l1) 1#u32
-          let ls ← list_nth_mut_back 3#i32
-          let i4 ← list_nth_shared I32 ls 0#u32
-          if i4 = 0#i32
+            list_nth_mut I32 (List.Cons 0i32 l1) 1u32
+          let ls ← list_nth_mut_back 3i32
+          let i4 ← list_nth_shared I32 ls 0u32
+          if i4 = 0i32
           then
             do
-            let i5 ← list_nth_shared I32 ls 1#u32
-            if i5 = 3#i32
+            let i5 ← list_nth_shared I32 ls 1u32
+            if i5 = 3i32
             then
               do
-              let i6 ← list_nth_shared I32 ls 2#u32
-              if i6 = 2#i32
+              let i6 ← list_nth_shared I32 ls 2u32
+              if i6 = 2i32
               then Result.ok ()
               else Result.fail .panic
             else Result.fail .panic
@@ -425,17 +425,17 @@ structure StructWithTuple (T1 T2 : Type) where
 /- [no_nested_borrows::new_tuple1]:
    Source: 'tests/src/no_nested_borrows.rs', lines 363:0-363:48 -/
 def new_tuple1 : Result (StructWithTuple U32 U32) :=
-  Result.ok { p := (1#u32, 2#u32) }
+  Result.ok { p := (1u32, 2u32) }
 
 /- [no_nested_borrows::new_tuple2]:
    Source: 'tests/src/no_nested_borrows.rs', lines 367:0-367:48 -/
 def new_tuple2 : Result (StructWithTuple I16 I16) :=
-  Result.ok { p := (1#i16, 2#i16) }
+  Result.ok { p := (1i16, 2i16) }
 
 /- [no_nested_borrows::new_tuple3]:
    Source: 'tests/src/no_nested_borrows.rs', lines 371:0-371:48 -/
 def new_tuple3 : Result (StructWithTuple U64 I64) :=
-  Result.ok { p := (1#u64, 2#i64) }
+  Result.ok { p := (1u64, 2i64) }
 
 /- [no_nested_borrows::StructWithPair]
    Source: 'tests/src/no_nested_borrows.rs', lines 376:0-376:33 -/
@@ -445,7 +445,7 @@ structure StructWithPair (T1 T2 : Type) where
 /- [no_nested_borrows::new_pair1]:
    Source: 'tests/src/no_nested_borrows.rs', lines 380:0-380:46 -/
 def new_pair1 : Result (StructWithPair U32 U32) :=
-  Result.ok { p := { x := 1#u32, y := 2#u32 } }
+  Result.ok { p := { x := 1u32, y := 2u32 } }
 
 /- [no_nested_borrows::test_constants]:
    Source: 'tests/src/no_nested_borrows.rs', lines 388:0-388:23 -/
@@ -453,21 +453,21 @@ def test_constants : Result Unit :=
   do
   let swt ← new_tuple1
   let (i, _) := swt.p
-  if i = 1#u32
+  if i = 1u32
   then
     do
     let swt1 ← new_tuple2
     let (i1, _) := swt1.p
-    if i1 = 1#i16
+    if i1 = 1i16
     then
       do
       let swt2 ← new_tuple3
       let (i2, _) := swt2.p
-      if i2 = 1#u64
+      if i2 = 1u64
       then
         do
         let swp ← new_pair1
-        if swp.p.x = 1#u32
+        if swp.p.x = 1u32
         then Result.ok ()
         else Result.fail .panic
       else Result.fail .panic
@@ -488,39 +488,39 @@ def test_weird_borrows1 : Result Unit :=
 /- [no_nested_borrows::test_mem_replace]:
    Source: 'tests/src/no_nested_borrows.rs', lines 407:0-407:37 -/
 def test_mem_replace (px : U32) : Result U32 :=
-  let (y, _) := core.mem.replace U32 px 1#u32
-  if y = 0#u32
-  then Result.ok 2#u32
+  let (y, _) := core.mem.replace U32 px 1u32
+  if y = 0u32
+  then Result.ok 2u32
   else Result.fail .panic
 
 /- [no_nested_borrows::test_shared_borrow_bool1]:
    Source: 'tests/src/no_nested_borrows.rs', lines 414:0-414:47 -/
 def test_shared_borrow_bool1 (b : Bool) : Result U32 :=
   if b
-  then Result.ok 0#u32
-  else Result.ok 1#u32
+  then Result.ok 0u32
+  else Result.ok 1u32
 
 /- [no_nested_borrows::test_shared_borrow_bool2]:
    Source: 'tests/src/no_nested_borrows.rs', lines 427:0-427:40 -/
 def test_shared_borrow_bool2 : Result U32 :=
-  Result.ok 0#u32
+  Result.ok 0u32
 
 /- [no_nested_borrows::test_shared_borrow_enum1]:
    Source: 'tests/src/no_nested_borrows.rs', lines 442:0-442:52 -/
 def test_shared_borrow_enum1 (l : List U32) : Result U32 :=
   match l with
-  | List.Cons _ _ => Result.ok 1#u32
-  | List.Nil => Result.ok 0#u32
+  | List.Cons _ _ => Result.ok 1u32
+  | List.Nil => Result.ok 0u32
 
 /- [no_nested_borrows::test_shared_borrow_enum2]:
    Source: 'tests/src/no_nested_borrows.rs', lines 454:0-454:40 -/
 def test_shared_borrow_enum2 : Result U32 :=
-  Result.ok 0#u32
+  Result.ok 0u32
 
 /- [no_nested_borrows::incr]:
    Source: 'tests/src/no_nested_borrows.rs', lines 465:0-465:24 -/
 def incr (x : U32) : Result U32 :=
-  x + 1#u32
+  x + 1u32
 
 /- [no_nested_borrows::call_incr]:
    Source: 'tests/src/no_nested_borrows.rs', lines 469:0-469:35 -/
@@ -531,7 +531,7 @@ def call_incr (x : U32) : Result U32 :=
    Source: 'tests/src/no_nested_borrows.rs', lines 474:0-474:41 -/
 def read_then_incr (x : U32) : Result (U32 × U32) :=
   do
-  let x1 ← x + 1#u32
+  let x1 ← x + 1u32
   Result.ok (x, x1)
 
 /- [no_nested_borrows::Tuple]
@@ -548,7 +548,7 @@ def read_tuple (x : (U32 × U32)) : Result U32 :=
    Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:39 -/
 def update_tuple (x : (U32 × U32)) : Result (U32 × U32) :=
   let (_, i) := x
-  Result.ok (1#u32, i)
+  Result.ok (1u32, i)
 
 /- [no_nested_borrows::read_tuple_struct]:
    Source: 'tests/src/no_nested_borrows.rs', lines 490:0-490:52 -/
@@ -560,7 +560,7 @@ def read_tuple_struct (x : Tuple U32 U32) : Result U32 :=
    Source: 'tests/src/no_nested_borrows.rs', lines 494:0-494:51 -/
 def update_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) :=
   let (_, i) := x
-  Result.ok (1#u32, i)
+  Result.ok (1u32, i)
 
 /- [no_nested_borrows::create_tuple_struct]:
    Source: 'tests/src/no_nested_borrows.rs', lines 498:0-498:61 -/
-- 
cgit v1.2.3