Merge pull request #246 from AeneasVerif/son/cleanup

Do some cleanup in the test files and the Lean backend

1 files changed, 14 insertions, 0 deletions

diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 199605d5..e676336e 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -2,6 +2,9 @@
 -- [loops]
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace loops
 
@@ -110,6 +113,7 @@ divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
 
 /- [loops::list_mem]:
    Source: 'tests/src/loops.rs', lines 80:0-80:52 -/
+@[reducible]
 def list_mem (x : U32) (ls : List U32) : Result Bool :=
   list_mem_loop x ls
 
@@ -136,6 +140,7 @@ divergent def list_nth_mut_loop_loop
 
 /- [loops::list_nth_mut_loop]:
    Source: 'tests/src/loops.rs', lines 92:0-92:71 -/
+@[reducible]
 def list_nth_mut_loop
   (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
   list_nth_mut_loop_loop T ls i
@@ -155,6 +160,7 @@ divergent def list_nth_shared_loop_loop
 
 /- [loops::list_nth_shared_loop]:
    Source: 'tests/src/loops.rs', lines 105:0-105:66 -/
+@[reducible]
 def list_nth_shared_loop (T : Type) (ls : List T) (i : U32) : Result T :=
   list_nth_shared_loop_loop T ls i
 
@@ -316,6 +322,7 @@ divergent def list_nth_mut_loop_pair_loop
 
 /- [loops::list_nth_mut_loop_pair]:
    Source: 'tests/src/loops.rs', lines 188:0-192:27 -/
+@[reducible]
 def list_nth_mut_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)) × (T → Result (List T)))
@@ -340,6 +347,7 @@ divergent def list_nth_shared_loop_pair_loop
 
 /- [loops::list_nth_shared_loop_pair]:
    Source: 'tests/src/loops.rs', lines 212:0-216:19 -/
+@[reducible]
 def list_nth_shared_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   list_nth_shared_loop_pair_loop T ls0 ls1 i
@@ -376,6 +384,7 @@ divergent def list_nth_mut_loop_pair_merge_loop
 
 /- [loops::list_nth_mut_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 237:0-241:27 -/
+@[reducible]
 def list_nth_mut_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × ((T × T) → Result ((List T) × (List T))))
@@ -401,6 +410,7 @@ divergent def list_nth_shared_loop_pair_merge_loop
 
 /- [loops::list_nth_shared_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 255:0-259:19 -/
+@[reducible]
 def list_nth_shared_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
   list_nth_shared_loop_pair_merge_loop T ls0 ls1 i
@@ -433,6 +443,7 @@ divergent def list_nth_mut_shared_loop_pair_loop
 
 /- [loops::list_nth_mut_shared_loop_pair]:
    Source: 'tests/src/loops.rs', lines 273:0-277:23 -/
+@[reducible]
 def list_nth_mut_shared_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -467,6 +478,7 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
 
 /- [loops::list_nth_mut_shared_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 292:0-296:23 -/
+@[reducible]
 def list_nth_mut_shared_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -501,6 +513,7 @@ divergent def list_nth_shared_mut_loop_pair_loop
 
 /- [loops::list_nth_shared_mut_loop_pair]:
    Source: 'tests/src/loops.rs', lines 311:0-315:23 -/
+@[reducible]
 def list_nth_shared_mut_loop_pair
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))
@@ -535,6 +548,7 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
 
 /- [loops::list_nth_shared_mut_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 330:0-334:23 -/
+@[reducible]
 def list_nth_shared_mut_loop_pair_merge
   (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
   Result ((T × T) × (T → Result (List T)))