Regenerate the tests

26 files changed, 77 insertions, 2 deletions

diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index 9748919e..bb97d5c4 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -2,6 +2,9 @@
 -- [arrays]
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace arrays
 
diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean
index 05341b31..4592e91c 100644
--- a/tests/lean/Betree/Funs.lean
+++ b/tests/lean/Betree/Funs.lean
@@ -4,6 +4,9 @@ import Base
 import Betree.Types
 import Betree.FunsExternal
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace betree
 
diff --git a/tests/lean/Betree/FunsExternal_Template.lean b/tests/lean/Betree/FunsExternal_Template.lean
index 014f0d83..2fb40ebc 100644
--- a/tests/lean/Betree/FunsExternal_Template.lean
+++ b/tests/lean/Betree/FunsExternal_Template.lean
@@ -4,6 +4,9 @@
 import Base
 import Betree.Types
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 open betree
 
 /- [betree::betree_utils::load_internal_node]:
diff --git a/tests/lean/Betree/Types.lean b/tests/lean/Betree/Types.lean
index 3b46c00c..9e7c505b 100644
--- a/tests/lean/Betree/Types.lean
+++ b/tests/lean/Betree/Types.lean
@@ -3,6 +3,9 @@
 import Base
 import Betree.TypesExternal
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace betree
 
diff --git a/tests/lean/Betree/TypesExternal_Template.lean b/tests/lean/Betree/TypesExternal_Template.lean
index 12fce657..f97517a6 100644
--- a/tests/lean/Betree/TypesExternal_Template.lean
+++ b/tests/lean/Betree/TypesExternal_Template.lean
@@ -3,6 +3,9 @@
 -- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 /- The state type used in the state-error monad -/
 axiom State : Type
diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean
index 23ec66b4..7f347661 100644
--- a/tests/lean/Bitwise.lean
+++ b/tests/lean/Bitwise.lean
@@ -2,6 +2,9 @@
 -- [bitwise]
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace bitwise
 
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index ecb91c16..fff74646 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -2,6 +2,9 @@
 -- [constants]
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace constants
 
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 2bbc385d..a557cf73 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -2,6 +2,9 @@
 -- [demo]
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace demo
 
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 1b1d5cdf..cd1883e5 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -4,6 +4,9 @@ import Base
 import External.Types
 import External.FunsExternal
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace external
 
diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean
index 870a79c0..51050b21 100644
--- a/tests/lean/External/FunsExternal_Template.lean
+++ b/tests/lean/External/FunsExternal_Template.lean
@@ -4,6 +4,9 @@
 import Base
 import External.Types
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 open external
 
 /- [core::cell::{core::cell::Cell<T>#10}::get]:
diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean
index 836ddff0..50446e1c 100644
--- a/tests/lean/External/Types.lean
+++ b/tests/lean/External/Types.lean
@@ -3,6 +3,9 @@
 import Base
 import External.TypesExternal
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace external
 
diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean
index 24687d83..2cfbcc80 100644
--- a/tests/lean/External/TypesExternal_Template.lean
+++ b/tests/lean/External/TypesExternal_Template.lean
@@ -3,6 +3,9 @@
 -- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 /- [core::cell::Cell]
    Source: '/rustc/65ea825f4021eaf77f1b25139969712d65b435a4/library/core/src/cell.rs', lines 294:0-294:26
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index f5d028db..7972b715 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -4,6 +4,9 @@ import Base
 import Hashmap.Types
 import Hashmap.FunsExternal
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace hashmap
 
diff --git a/tests/lean/Hashmap/FunsExternal_Template.lean b/tests/lean/Hashmap/FunsExternal_Template.lean
index 80362a92..ea5ceed3 100644
--- a/tests/lean/Hashmap/FunsExternal_Template.lean
+++ b/tests/lean/Hashmap/FunsExternal_Template.lean
@@ -4,6 +4,9 @@
 import Base
 import Hashmap.Types
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 open hashmap
 
 /- [hashmap::utils::deserialize]:
diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean
index 93af883e..6f5d99a5 100644
--- a/tests/lean/Hashmap/Types.lean
+++ b/tests/lean/Hashmap/Types.lean
@@ -3,6 +3,9 @@
 import Base
 import Hashmap.TypesExternal
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace hashmap
 
diff --git a/tests/lean/Hashmap/TypesExternal_Template.lean b/tests/lean/Hashmap/TypesExternal_Template.lean
index 03c3d157..b6f24513 100644
--- a/tests/lean/Hashmap/TypesExternal_Template.lean
+++ b/tests/lean/Hashmap/TypesExternal_Template.lean
@@ -3,6 +3,9 @@
 -- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 /- The state type used in the state-error monad -/
 axiom State : Type
diff --git a/tests/lean/InfiniteLoop.lean b/tests/lean/InfiniteLoop.lean
index b8c2343e..b5986ed8 100644
--- a/tests/lean/InfiniteLoop.lean
+++ b/tests/lean/InfiniteLoop.lean
@@ -2,6 +2,9 @@
 -- [infinite_loop]
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace infinite_loop
 
diff --git a/tests/lean/Issue194RecursiveStructProjector.lean b/tests/lean/Issue194RecursiveStructProjector.lean
index 4eb23934..730d1aa6 100644
--- a/tests/lean/Issue194RecursiveStructProjector.lean
+++ b/tests/lean/Issue194RecursiveStructProjector.lean
@@ -2,6 +2,9 @@
 -- [issue_194_recursive_struct_projector]
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace issue_194_recursive_struct_projector
 
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index a9e5a499..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
 
diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean
index 9233841b..8d592a85 100644
--- a/tests/lean/Matches.lean
+++ b/tests/lean/Matches.lean
@@ -2,6 +2,9 @@
 -- [matches]
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace matches
 
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index f0438050..090ca2b2 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -2,6 +2,9 @@
 -- [no_nested_borrows]
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace no_nested_borrows
 
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 03b96903..b1aef703 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -2,6 +2,9 @@
 -- [paper]
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace paper
 
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index ed279d58..489871ba 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -2,6 +2,9 @@
 -- [polonius_list]
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace polonius_list
 
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index 0dd692fe..51aba5bf 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -2,6 +2,9 @@
 -- [traits]
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace traits
 
diff --git a/tests/lean/misc/MutuallyRecursiveTraits.lean b/tests/lean/misc/MutuallyRecursiveTraits.lean
index b0fcb9e9..05871009 100644
--- a/tests/lean/misc/MutuallyRecursiveTraits.lean
+++ b/tests/lean/misc/MutuallyRecursiveTraits.lean
@@ -2,5 +2,8 @@
 -- [mutually_recursive_traits]
 import Base
 open Primitives
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
 
 namespace mutually_recursive_traits
diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out
index e2ed3abc..9b3b0737 100644
--- a/tests/src/mutually-recursive-traits.lean.out
+++ b/tests/src/mutually-recursive-traits.lean.out
@@ -12,6 +12,6 @@ Uncaught exception:
 Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 46, characters 4-76
 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
 Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 836, characters 2-52
-Called from Aeneas__Translate.extract_file in file "Translate.ml", line 954, characters 2-36
-Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1503, characters 5-42
+Called from Aeneas__Translate.extract_file in file "Translate.ml", line 963, characters 2-36
+Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1512, characters 5-42
 Called from Dune__exe__Main in file "Main.ml", line 314, characters 14-66