From 62142c5a4a625f46e19fd3c63f206cc3ee23d2de Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Sun, 10 May 2026 10:58:04 -0700
Subject: [PATCH] chore: add missing `noexcept`s (#13370)

swap and move constructors should be noexcept to enable use in STL
containers

A quick inspection suggests that these functions can never throw
exceptions anyway.
---
 src/kernel/type_checker.cpp | 2 +-
 src/kernel/type_checker.h   | 2 +-
 src/runtime/mpz.cpp         | 8 ++++----
 src/runtime/mpz.h           | 4 ++--
 src/util/name_generator.cpp | 2 +-
 src/util/name_generator.h   | 4 ++--
 6 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index dd3741a339..e8b1ff5610 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -1170,7 +1170,7 @@ type_checker::type_checker(state & st, local_ctx const & lctx, definition_safety
     m_definition_safety(ds), m_lparams(nullptr) {
 }
 
-type_checker::type_checker(type_checker && src):
+type_checker::type_checker(type_checker && src) noexcept:
     m_st_owner(src.m_st_owner), m_st(src.m_st), m_diag(src.m_diag), m_lctx(std::move(src.m_lctx)),
     m_definition_safety(src.m_definition_safety), m_lparams(src.m_lparams) {
     src.m_st_owner = false;
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 32fb89d949..23b06a2873 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -116,7 +116,7 @@ public:
     type_checker(state & st, definition_safety ds = definition_safety::safe):type_checker(st, local_ctx(), ds) {}
     type_checker(environment const & env, local_ctx const & lctx, diagnostics * diag = nullptr, definition_safety ds = definition_safety::safe);
     type_checker(environment const & env, diagnostics * diag = nullptr, definition_safety ds = definition_safety::safe):type_checker(env, local_ctx(), diag, ds) {}
-    type_checker(type_checker &&);
+    type_checker(type_checker &&) noexcept;
     type_checker(type_checker const &) = delete;
     ~type_checker();
 
diff --git a/src/runtime/mpz.cpp b/src/runtime/mpz.cpp
index 54392490bf..afb754635d 100644
--- a/src/runtime/mpz.cpp
+++ b/src/runtime/mpz.cpp
@@ -61,7 +61,7 @@ mpz::mpz(mpz const & s) {
     mpz_init_set(m_val, s.m_val);
 }
 
-mpz::mpz(mpz && s):mpz() {
+mpz::mpz(mpz && s) noexcept : mpz() {
     mpz_swap(m_val, s.m_val);
 }
 
@@ -73,7 +73,7 @@ void mpz::set(mpz_t r) const {
     mpz_set(r, m_val);
 }
 
-void swap(mpz & a, mpz & b) {
+void swap(mpz & a, mpz & b) noexcept {
     mpz_swap(a.m_val, b.m_val);
 }
 
@@ -446,7 +446,7 @@ mpz::mpz(mpz const & s) {
     init_mpz(s);
 }
 
-mpz::mpz(mpz && s):
+mpz::mpz(mpz && s) noexcept :
     m_sign(s.m_sign),
     m_size(s.m_size),
     m_digits(s.m_digits) {
@@ -459,7 +459,7 @@ mpz::~mpz() {
     }
 }
 
-void swap(mpz & a, mpz & b) {
+void swap(mpz & a, mpz & b) noexcept {
     std::swap(a.m_sign, b.m_sign);
     std::swap(a.m_size, b.m_size);
     std::swap(a.m_digits, b.m_digits);
diff --git a/src/runtime/mpz.h b/src/runtime/mpz.h
index d8777f26d1..788b3f2509 100644
--- a/src/runtime/mpz.h
+++ b/src/runtime/mpz.h
@@ -62,14 +62,14 @@ public:
             return mpz((unsigned) v); // NOLINT
     }
     mpz(mpz const & s);
-    mpz(mpz && s);
+    mpz(mpz && s) noexcept;
     ~mpz();
 
 #ifdef LEAN_USE_GMP
     void set(mpz_t r) const;
 #endif
 
-    friend void swap(mpz & a, mpz & b);
+    friend void swap(mpz & a, mpz & b) noexcept;
 
     unsigned hash() const {
 #ifdef LEAN_USE_GMP
diff --git a/src/util/name_generator.cpp b/src/util/name_generator.cpp
index 1ac890b881..b6eb06bf52 100644
--- a/src/util/name_generator.cpp
+++ b/src/util/name_generator.cpp
@@ -48,7 +48,7 @@ name name_generator::next_with(name const & base_prefix) {
     return replace_base_prefix(next(), base_prefix);
 }
 
-void swap(name_generator & a, name_generator & b) {
+void swap(name_generator & a, name_generator & b) noexcept {
     swap(a.m_prefix, b.m_prefix);
     std::swap(a.m_next_idx, b.m_next_idx);
 }
diff --git a/src/util/name_generator.h b/src/util/name_generator.h
index acec5f04de..b2ccfc3b93 100644
--- a/src/util/name_generator.h
+++ b/src/util/name_generator.h
@@ -60,9 +60,9 @@ public:
        the current state of this object is updated to `m_next_idx = 11` */
     name_generator mk_child_with(name const & base_prefix) { return name_generator(next_with(base_prefix)); }
 
-    friend void swap(name_generator & a, name_generator & b);
+    friend void swap(name_generator & a, name_generator & b) noexcept;
 };
-void swap(name_generator & a, name_generator & b);
+void swap(name_generator & a, name_generator & b) noexcept;
 
 /* This procedure is invoked during initialization time to register
    internal prefixes used to create name_generator objects.