Simplify the generated names for the types in Lean

3 files changed, 4 insertions, 5 deletions

diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 6bfffc33..10efc3db 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -28,10 +28,10 @@ def swap_back
 
 /- [external::test_new_non_zero_u32] -/
 def test_new_non_zero_u32_fwd
-  (x : U32) (st : State) : Result (State × core_num_nonzero_non_zero_u32_t) :=
+  (x : U32) (st : State) : Result (State × core.num.nonzero.NonZeroU32) :=
   do
     let (st0, opt) ← core.num.nonzero.NonZeroU32.new_fwd x st
-    core.option.Option.unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0
+    core.option.Option.unwrap_fwd core.num.nonzero.NonZeroU32 opt st0
 
 /- [external::test_vec] -/
 def test_vec_fwd : Result Unit :=
diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean
index d6c0eb1d..669fe91b 100644
--- a/tests/lean/External/FunsExternal_Template.lean
+++ b/tests/lean/External/FunsExternal_Template.lean
@@ -20,8 +20,7 @@ axiom core.mem.swap_back1
 
 /- [core::num::nonzero::NonZeroU32::{14}::new] -/
 axiom core.num.nonzero.NonZeroU32.new_fwd
-  :
-  U32 → State → Result (State × (Option core_num_nonzero_non_zero_u32_t))
+  : U32 → State → Result (State × (Option core.num.nonzero.NonZeroU32))
 
 /- [core::option::Option::{0}::unwrap] -/
 axiom core.option.Option.unwrap_fwd
diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean
index 316f6474..ba984e2a 100644
--- a/tests/lean/External/Types.lean
+++ b/tests/lean/External/Types.lean
@@ -5,7 +5,7 @@ open Primitives
 namespace external
 
 /- [core::num::nonzero::NonZeroU32] -/
-axiom core_num_nonzero_non_zero_u32_t : Type
+axiom core.num.nonzero.NonZeroU32 : Type
 
 /- The state type used in the state-error monad -/
 axiom State : Type