chore: add missing noexcepts

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;

src/kernel/type_checker.h

@@ -116,7 +116,7 @@ class type_checker {
     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();
 

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):mpz() noexcept {
     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);
 }
 
@@ -441,7 +441,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) {
@@ -454,7 +454,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);

src/runtime/mpz.h

@@ -62,14 +62,14 @@ class LEAN_EXPORT mpz {
             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

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);
 }

src/util/name_generator.h

@@ -60,9 +60,9 @@ class name_generator {
        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.