From ab6ca82e6fb1e529646e22c5772722262da382c7 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Thu, 19 Sep 2013 21:26:01 -0700 Subject: [PATCH] Update to suppress unused-parameter warnings --- src/CMakeLists.txt | 2 +- src/frontends/lean/elaborator.cpp | 6 +-- src/frontends/lean/frontend.cpp | 2 +- src/frontends/lean/parser.cpp | 2 +- src/frontends/lean/pp.cpp | 4 +- src/kernel/expr.cpp | 2 +- src/kernel/metavar.cpp | 6 +-- src/kernel/object.h | 2 +- src/kernel/occurs.cpp | 4 +- src/kernel/replace.h | 2 +- src/library/arith/int.cpp | 2 +- src/library/arith/nat.cpp | 2 +- src/library/arith/real.cpp | 2 +- src/library/formatter.cpp | 10 ++--- src/library/formatter.h | 2 +- src/library/ho_unifier.cpp | 8 ++-- src/library/kernel_exception_formatter.cpp | 4 +- src/library/placeholder.cpp | 2 +- src/library/printer.cpp | 2 +- src/library/reduce.cpp | 2 +- src/shell/lean.cpp | 2 +- src/util/debug.cpp | 1 - src/util/interval/interval.h | 2 +- src/util/numerics/mpbq.h | 42 ++++++++++----------- src/util/numerics/mpfp.h | 22 +++++------ src/util/numerics/mpq.h | 44 +++++++++++----------- src/util/numerics/mpz.h | 2 +- 27 files changed, 91 insertions(+), 92 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 8d3494e42..20e9bfdcf 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -25,7 +25,7 @@ endif() set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules/") # Initialize CXXFLAGS. -set(CMAKE_CXX_FLAGS "-Wall -std=c++11 ${LEAN_EXTRA_CXX_FLAGS}") +set(CMAKE_CXX_FLAGS "-Wall -Wunused-parameter -std=c++11 ${LEAN_EXTRA_CXX_FLAGS}") set(CMAKE_CXX_FLAGS_DEBUG "-g -DLEAN_DEBUG -DLEAN_TRACE") set(CMAKE_CXX_FLAGS_MINSIZEREL "-Os -DNDEBUG") set(CMAKE_CXX_FLAGS_RELEASE "-O3 -DNDEBUG") diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index c81183d38..4a272164a 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -502,7 +502,7 @@ class elaborator::imp { struct cycle_detected {}; void occ_core(expr const & t) { check_interrupted(m_interrupted); - auto proc = [&](expr const & e, unsigned offset) { + auto proc = [&](expr const & e, unsigned) { if (is_metavar(e)) { unsigned midx = metavar_idx(e); if (m_metavars[midx].m_mark) @@ -741,7 +741,7 @@ class elaborator::imp { struct found_assigned {}; bool has_assigned_metavar(expr const & e) { - auto proc = [&](expr const & n, unsigned offset) { + auto proc = [&](expr const & n, unsigned) { if (is_metavar(n)) { unsigned midx = metavar_idx(n); if (m_metavars[midx].m_assignment) @@ -758,7 +758,7 @@ class elaborator::imp { } expr instantiate(expr const & e) { - auto proc = [&](expr const & n, unsigned offset) -> expr { + auto proc = [&](expr const & n, unsigned) -> expr { if (is_metavar(n)) { expr const & m = n; unsigned midx = metavar_idx(m); diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index ddcc9e2eb..c97a7d225 100644 --- a/src/frontends/lean/frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -347,7 +347,7 @@ struct frontend::imp { m_state.set_interrupt(flag); } - imp(frontend & fe): + imp(frontend &): m_num_children(0) { } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index baa66f9a0..0a410476f 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -704,7 +704,7 @@ class parser::imp { \remark If \c suppress_type is true, then the type doesn't need to be provided. That is, we automatically include a placeholder. */ - void parse_simple_bindings(bindings_buffer & result, bool implicit_decl, bool supress_type) { + void parse_simple_bindings(bindings_buffer & result, bool implicit_decl, bool suppress_type) { buffer> names; parse_names(names); expr type; diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index e4d461915..b034051d5 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1106,7 +1106,7 @@ class pp_fn { struct found_prefix {}; bool uses_prefix(expr const & e, name const & prefix) { - auto f = [&](expr const & e, unsigned offset) { + auto f = [&](expr const & e, unsigned) { if (is_constant(e)) { if (is_prefix_of(prefix, const_name(e))) throw found_prefix(); } else if (is_abstraction(e)) { @@ -1274,7 +1274,7 @@ class pp_formatter_cell : public formatter_cell { return r; } - format pp_builtin_set(object const & obj, options const & opts) { + format pp_builtin_set(object const & obj, options const &) { char const * kwd = obj.keyword(); name const & n = obj.get_name(); return format{highlight_command(format(kwd)), space(), format(n)}; diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 5594d7c66..030429dfb 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -108,7 +108,7 @@ expr_let::expr_let(name const & n, expr const & t, expr const & v, expr const & } expr_let::~expr_let() {} name value::get_unicode_name() const { return get_name(); } -bool value::normalize(unsigned num_args, expr const * args, expr & r) const { return false; } +bool value::normalize(unsigned, expr const *, expr &) const { return false; } void value::display(std::ostream & out) const { out << get_name(); } bool value::operator==(value const & other) const { return typeid(*this) == typeid(other); } format value::pp() const { return format(get_name()); } diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index f75109589..5d7dada1a 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -129,7 +129,7 @@ expr instantiate_metavars(expr const & e, metavar_env const & env) { if (!has_metavar(e)) { return e; } else { - auto f = [=](expr const & m, unsigned offset) -> expr { + auto f = [=](expr const & m, unsigned) -> expr { if (is_metavar(m) && env.contains(m)) { expr s = env.get_subst(m); return s ? s : m; @@ -195,7 +195,7 @@ bool has_assigned_metavar(expr const & e, metavar_env const & menv) { if (!has_metavar(e)) { return false; } else { - auto proc = [&](expr const & n, unsigned offset) { + auto proc = [&](expr const & n, unsigned) { if (is_metavar(n) && menv.contains(n) && menv.is_assigned(n)) throw found_assigned(); }; @@ -216,7 +216,7 @@ bool has_assigned_metavar(expr const & e, metavar_env const & menv) { struct found_metavar {}; bool has_metavar(expr const & e, unsigned midx, metavar_env const & menv) { - auto f = [&](expr const & m, unsigned offset) { + auto f = [&](expr const & m, unsigned) { if (is_metavar(m)) { unsigned midx2 = metavar_idx(m); if (midx2 == midx) diff --git a/src/kernel/object.h b/src/kernel/object.h index f54e5fcd3..2f1bf205c 100644 --- a/src/kernel/object.h +++ b/src/kernel/object.h @@ -61,7 +61,7 @@ public: virtual bool is_theorem() const { return false; } virtual bool is_var_decl() const { return false; } - virtual bool in_builtin_set(expr const & v) const { return false; } + virtual bool in_builtin_set(expr const &) const { return false; } }; /** diff --git a/src/kernel/occurs.cpp b/src/kernel/occurs.cpp index 96b3ddb7c..fd6a2a8cd 100644 --- a/src/kernel/occurs.cpp +++ b/src/kernel/occurs.cpp @@ -27,7 +27,7 @@ namespace occurs_ns { struct found {}; } bool occurs(name const & n, context const * c, unsigned sz, expr const * es) { - auto visitor = [&](expr const & e, unsigned offset) -> void { + auto visitor = [&](expr const & e, unsigned) -> void { if (is_constant(e)) { if (const_name(e) == n) throw occurs_ns::found(); @@ -42,7 +42,7 @@ bool occurs(name const & n, context const * c, unsigned sz, expr const * es) { } bool occurs(expr const & n, context const * c, unsigned sz, expr const * es) { - auto visitor = [&](expr const & e, unsigned offset) -> void { + auto visitor = [&](expr const & e, unsigned) -> void { if (e == n) throw occurs_ns::found(); }; diff --git a/src/kernel/replace.h b/src/kernel/replace.h index 6d0bfe684..1b866a126 100644 --- a/src/kernel/replace.h +++ b/src/kernel/replace.h @@ -16,7 +16,7 @@ namespace lean { */ class default_replace_postprocessor { public: - void operator()(expr const & old_e, expr const & new_e) {} + void operator()(expr const &, expr const &) {} }; /** diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp index 909fc561a..780ef3ed8 100644 --- a/src/library/arith/int.cpp +++ b/src/library/arith/int.cpp @@ -34,7 +34,7 @@ public: } virtual void display(std::ostream & out) const { out << m_val; } virtual format pp() const { return format(m_val); } - virtual format pp(bool unicode) const { return pp(); } + virtual format pp(bool ) const { return pp(); } virtual unsigned hash() const { return m_val.hash(); } mpz const & get_num() const { return m_val; } }; diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp index 10675fd86..535b49ea3 100644 --- a/src/library/arith/nat.cpp +++ b/src/library/arith/nat.cpp @@ -33,7 +33,7 @@ public: } virtual void display(std::ostream & out) const { out << m_val; } virtual format pp() const { return format(m_val); } - virtual format pp(bool unicode) const { return pp(); } + virtual format pp(bool ) const { return pp(); } virtual unsigned hash() const { return m_val.hash(); } mpz const & get_num() const { return m_val; } }; diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp index 96b56d765..76c6e81d7 100644 --- a/src/library/arith/real.cpp +++ b/src/library/arith/real.cpp @@ -37,7 +37,7 @@ public: } virtual void display(std::ostream & out) const { out << m_val; } virtual format pp() const { return format(m_val); } - virtual format pp(bool unicode) const { return pp(); } + virtual format pp(bool ) const { return pp(); } virtual unsigned hash() const { return m_val.hash(); } mpq const & get_num() const { return m_val; } }; diff --git a/src/library/formatter.cpp b/src/library/formatter.cpp index 975d728e4..d8559ce60 100644 --- a/src/library/formatter.cpp +++ b/src/library/formatter.cpp @@ -12,23 +12,23 @@ Author: Leonardo de Moura namespace lean { class simple_formatter_cell : public formatter_cell { public: - virtual format operator()(expr const & e, options const & opts) { + virtual format operator()(expr const & e, options const &) { std::ostringstream s; s << e; return format(s.str()); } - virtual format operator()(context const & c, options const & opts) { + virtual format operator()(context const & c, options const &) { std::ostringstream s; s << c; return format(s.str()); } - virtual format operator()(context const & c, expr const & e, bool format_ctx, options const & opts) { + virtual format operator()(context const & c, expr const & e, bool format_ctx, options const &) { std::ostringstream s; if (format_ctx) s << c << "|-\n"; s << mk_pair(e, c); return format(s.str()); } - virtual format operator()(object const & obj, options const & opts) { + virtual format operator()(object const & obj, options const &) { std::ostringstream s; s << obj; return format(s.str()); } - virtual format operator()(environment const & env, options const & opts) { + virtual format operator()(environment const & env, options const &) { std::ostringstream s; s << env; return format(s.str()); } }; diff --git a/src/library/formatter.h b/src/library/formatter.h index 357e431dc..2a8c34251 100644 --- a/src/library/formatter.h +++ b/src/library/formatter.h @@ -35,7 +35,7 @@ public: /** \brief Format the given environment */ virtual format operator()(environment const & env, options const & opts) = 0; /** \brief Request interruption */ - virtual void set_interrupt(bool flag) {} + virtual void set_interrupt(bool ) {} }; /** \brief Smart-pointer for the actual formatter object (aka \c formatter_cell). diff --git a/src/library/ho_unifier.cpp b/src/library/ho_unifier.cpp index 038cbfb4c..d47878715 100644 --- a/src/library/ho_unifier.cpp +++ b/src/library/ho_unifier.cpp @@ -285,7 +285,7 @@ class ho_unifier::imp { } /** \brief Creates a subproblem based on the application arguments */ - bool process_app_args(context const & ctx, expr const & a, expr const & b, unsigned start) { + bool process_app_args(context const & ctx, expr const & a, expr const & b, unsigned) { lean_assert(is_app(a) && is_app(b)); if (num_args(a) != num_args(b)) { return false; @@ -328,9 +328,9 @@ class ho_unifier::imp { bool m_failed; public: unification_problems_wrapper():m_failed(false) {} - virtual void add_eq(context const & ctx, expr const & lhs, expr const & rhs) { m_failed = true; } - virtual void add_type_of_eq(context const & ctx, expr const & n, expr const & t) { m_failed = true; } - virtual void add_is_convertible(context const & ctx, expr const & t1, expr const & t2) { m_failed = true; } + virtual void add_eq(context const &, expr const &, expr const &) { m_failed = true; } + virtual void add_type_of_eq(context const &, expr const &, expr const &) { m_failed = true; } + virtual void add_is_convertible(context const &, expr const &, expr const &) { m_failed = true; } bool failed() const { return m_failed; } }; diff --git a/src/library/kernel_exception_formatter.cpp b/src/library/kernel_exception_formatter.cpp index 5c198608e..2c02619e9 100644 --- a/src/library/kernel_exception_formatter.cpp +++ b/src/library/kernel_exception_formatter.cpp @@ -30,11 +30,11 @@ format pp(formatter const & fmt, kernel_exception const & ex, options const & op return format(ex.what()); } -format pp(unknown_name_exception const & ex, options const & opts) { +format pp(unknown_name_exception const & ex, options const &) { return format{format("unknown object '"), format(ex.get_name()), format("'")}; } -format pp(already_declared_exception const & ex, options const & opts) { +format pp(already_declared_exception const & ex, options const &) { return format{format("invalid object declaration, environment already has an object named '"), format(ex.get_name()), format("'")}; } diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp index dc63673ab..0201680a4 100644 --- a/src/library/placeholder.cpp +++ b/src/library/placeholder.cpp @@ -26,7 +26,7 @@ bool has_placeholder(expr const & e) { } expr replace_placeholders_with_metavars(expr const & e, metavar_env & menv, expr_map * trace) { - auto f = [&](expr const & e, context const & ctx, unsigned offset) -> expr { + auto f = [&](expr const & e, context const & ctx, unsigned) -> expr { if (is_placeholder(e)) { return menv.mk_metavar(ctx); } else { diff --git a/src/library/printer.cpp b/src/library/printer.cpp index 9d0a4336e..6fa0bffbd 100644 --- a/src/library/printer.cpp +++ b/src/library/printer.cpp @@ -75,7 +75,7 @@ struct print_expr_fn { return print_child(a, c); } - void print_metavar(expr const & a, context const & c) { + void print_metavar(expr const & a, context const &) { out() << "?M" << metavar_idx(a); if (metavar_ctx(a)) { out() << "["; diff --git a/src/library/reduce.cpp b/src/library/reduce.cpp index 343e0d5a7..4eda5bcd3 100644 --- a/src/library/reduce.cpp +++ b/src/library/reduce.cpp @@ -45,7 +45,7 @@ expr head_beta_reduce(expr const & t) { } expr beta_reduce(expr t) { - auto f = [=](expr const & m, unsigned offset) -> expr { + auto f = [=](expr const & m, unsigned) -> expr { if (is_head_beta(m)) return head_beta_reduce(m); else diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index fcafa8bd4..0ffb7e9f8 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -20,7 +20,7 @@ using lean::parser; static interruptable_ptr g_lean_shell; -static void on_ctrl_c(int i) { +static void on_ctrl_c(int ) { g_lean_shell.set_interrupt(true); } diff --git a/src/util/debug.cpp b/src/util/debug.cpp index 2632db692..958736dc4 100644 --- a/src/util/debug.cpp +++ b/src/util/debug.cpp @@ -90,7 +90,6 @@ void invoke_debugger() { } else { std::cerr << "ERROR STARTING GDB...\n"; // forcing seg fault. - int * x = 0; *x = 0; } return; diff --git a/src/util/interval/interval.h b/src/util/interval/interval.h index eef79c82d..b32683d32 100644 --- a/src/util/interval/interval.h +++ b/src/util/interval/interval.h @@ -321,7 +321,7 @@ public: friend interval cosh (interval o) { o.cosh(); return o; } friend interval cosh (interval o, interval_deps & deps) { o.cosh(deps); return o; } - friend interval cosh_jst(interval o, interval_deps & deps) { o.cosh(); return o; } + friend interval cosh_jst(interval o, interval_deps & deps) { o.cosh_jst(deps); return o; } friend interval tanh (interval o) { o.tanh(); return o; } friend interval tanh (interval o, interval_deps & deps) { o.tanh(deps); return o; } diff --git a/src/util/numerics/mpbq.h b/src/util/numerics/mpbq.h index 4507112ad..64fb1ab68 100644 --- a/src/util/numerics/mpbq.h +++ b/src/util/numerics/mpbq.h @@ -280,27 +280,27 @@ public: static void power(mpbq & v, unsigned k) { _power(v, v, k); } // Transcendental functions - static void exp(mpbq & v) { lean_unreachable(); } - static void exp2(mpbq & v) { lean_unreachable(); } - static void exp10(mpbq & v) { lean_unreachable(); } - static void log(mpbq & v) { lean_unreachable(); } - static void log2(mpbq & v) { lean_unreachable(); } - static void log10(mpbq & v) { lean_unreachable(); } - static void sin(mpbq & v) { lean_unreachable(); } - static void cos(mpbq & v) { lean_unreachable(); } - static void tan(mpbq & v) { lean_unreachable(); } - static void sec(mpbq & v) { lean_unreachable(); } - static void csc(mpbq & v) { lean_unreachable(); } - static void cot(mpbq & v) { lean_unreachable(); } - static void asin(mpbq & v) { lean_unreachable(); } - static void acos(mpbq & v) { lean_unreachable(); } - static void atan(mpbq & v) { lean_unreachable(); } - static void sinh(mpbq & v) { lean_unreachable(); } - static void cosh(mpbq & v) { lean_unreachable(); } - static void tanh(mpbq & v) { lean_unreachable(); } - static void asinh(mpbq & v) { lean_unreachable(); } - static void acosh(mpbq & v) { lean_unreachable(); } - static void atanh(mpbq & v) { lean_unreachable(); } + static void exp(mpbq & ) { lean_unreachable(); } + static void exp2(mpbq & ) { lean_unreachable(); } + static void exp10(mpbq & ) { lean_unreachable(); } + static void log(mpbq & ) { lean_unreachable(); } + static void log2(mpbq & ) { lean_unreachable(); } + static void log10(mpbq & ) { lean_unreachable(); } + static void sin(mpbq & ) { lean_unreachable(); } + static void cos(mpbq & ) { lean_unreachable(); } + static void tan(mpbq & ) { lean_unreachable(); } + static void sec(mpbq & ) { lean_unreachable(); } + static void csc(mpbq & ) { lean_unreachable(); } + static void cot(mpbq & ) { lean_unreachable(); } + static void asin(mpbq & ) { lean_unreachable(); } + static void acos(mpbq & ) { lean_unreachable(); } + static void atan(mpbq & ) { lean_unreachable(); } + static void sinh(mpbq & ) { lean_unreachable(); } + static void cosh(mpbq & ) { lean_unreachable(); } + static void tanh(mpbq & ) { lean_unreachable(); } + static void asinh(mpbq & ) { lean_unreachable(); } + static void acosh(mpbq & ) { lean_unreachable(); } + static void atanh(mpbq & ) { lean_unreachable(); } }; } diff --git a/src/util/numerics/mpfp.h b/src/util/numerics/mpfp.h index 04e321b17..9a72b09d9 100644 --- a/src/util/numerics/mpfp.h +++ b/src/util/numerics/mpfp.h @@ -33,37 +33,37 @@ public: // Setter functions mpfp & set(mpfp const & v, mpfr_rnd_t rnd = MPFR_RNDN) { - mpfr_set(m_val, v.m_val, MPFR_RNDN); return *this; + mpfr_set(m_val, v.m_val, rnd); return *this; } mpfp & set(unsigned long int const v, mpfr_rnd_t rnd = MPFR_RNDN) { - mpfr_set_ui(m_val, v, MPFR_RNDN); return *this; + mpfr_set_ui(m_val, v, rnd); return *this; } mpfp & set(long int const v, mpfr_rnd_t rnd = MPFR_RNDN) { - mpfr_set_si(m_val, v, MPFR_RNDN); return *this; + mpfr_set_si(m_val, v, rnd); return *this; } mpfp & set(float const v, mpfr_rnd_t rnd = MPFR_RNDN) { - mpfr_set_flt(m_val, v, MPFR_RNDN); return *this; + mpfr_set_flt(m_val, v, rnd); return *this; } mpfp & set(double const v, mpfr_rnd_t rnd = MPFR_RNDN) { - mpfr_set_d(m_val, v, MPFR_RNDN); return *this; + mpfr_set_d(m_val, v, rnd); return *this; } mpfp & set(long double const v, mpfr_rnd_t rnd = MPFR_RNDN) { - mpfr_set_ld(m_val, v, MPFR_RNDN); return *this; + mpfr_set_ld(m_val, v, rnd); return *this; } mpfp & set(mpz_t const & v, mpfr_rnd_t rnd = MPFR_RNDN) { - mpfr_set_z(m_val, v, MPFR_RNDN); return *this; + mpfr_set_z(m_val, v, rnd); return *this; } mpfp & set(mpq_t const & v, mpfr_rnd_t rnd = MPFR_RNDN) { - mpfr_set_q(m_val, v, MPFR_RNDN); return *this; + mpfr_set_q(m_val, v, rnd); return *this; } mpfp & set(mpf_t const & v, mpfr_rnd_t rnd = MPFR_RNDN) { - mpfr_set_f(m_val, v, MPFR_RNDN); return *this; + mpfr_set_f(m_val, v, rnd); return *this; } mpfp & set(mpz const & v, mpfr_rnd_t rnd = MPFR_RNDN) { - mpfr_set_z(m_val, v.m_val, MPFR_RNDN); return *this; + mpfr_set_z(m_val, v.m_val, rnd); return *this; } mpfp & set(mpq const & v, mpfr_rnd_t rnd = MPFR_RNDN) { - mpfr_set_q(m_val, v.m_val, MPFR_RNDN); return *this; + mpfr_set_q(m_val, v.m_val, rnd); return *this; } mpfp & set(mpbq const & v, mpfr_rnd_t rnd = MPFR_RNDN) { mpfr_set_z(m_val, v.m_num.m_val, rnd); // this = m_num diff --git a/src/util/numerics/mpq.h b/src/util/numerics/mpq.h index c8c10f7a3..d87692324 100644 --- a/src/util/numerics/mpq.h +++ b/src/util/numerics/mpq.h @@ -227,7 +227,7 @@ public: static bool is_zero(mpq const & v) { return v.is_zero(); } static bool is_pos(mpq const & v) { return v.is_pos(); } static bool is_neg(mpq const & v) { return v.is_neg(); } - static void set_rounding(bool plus_inf) {} + static void set_rounding(bool ) {} static void neg(mpq & v) { v.neg(); } static void inv(mpq & v) { v.inv(); } static void reset(mpq & v) { v = 0; } @@ -252,27 +252,27 @@ public: static inline mpq pi_twice_upper() { return pi_u * 2; } // Transcendental functions - static void exp(mpq & v) { lean_unreachable(); } - static void exp2(mpq & v) { lean_unreachable(); } - static void exp10(mpq & v) { lean_unreachable(); } - static void log(mpq & v) { lean_unreachable(); } - static void log2(mpq & v) { lean_unreachable(); } - static void log10(mpq & v) { lean_unreachable(); } - static void sin(mpq & v) { lean_unreachable(); } - static void cos(mpq & v) { lean_unreachable(); } - static void tan(mpq & v) { lean_unreachable(); } - static void sec(mpq & v) { lean_unreachable(); } - static void csc(mpq & v) { lean_unreachable(); } - static void cot(mpq & v) { lean_unreachable(); } - static void asin(mpq & v) { lean_unreachable(); } - static void acos(mpq & v) { lean_unreachable(); } - static void atan(mpq & v) { lean_unreachable(); } - static void sinh(mpq & v) { lean_unreachable(); } - static void cosh(mpq & v) { lean_unreachable(); } - static void tanh(mpq & v) { lean_unreachable(); } - static void asinh(mpq & v) { lean_unreachable(); } - static void acosh(mpq & v) { lean_unreachable(); } - static void atanh(mpq & v) { lean_unreachable(); } + static void exp(mpq & ) { lean_unreachable(); } + static void exp2(mpq & ) { lean_unreachable(); } + static void exp10(mpq & ) { lean_unreachable(); } + static void log(mpq & ) { lean_unreachable(); } + static void log2(mpq & ) { lean_unreachable(); } + static void log10(mpq & ) { lean_unreachable(); } + static void sin(mpq & ) { lean_unreachable(); } + static void cos(mpq & ) { lean_unreachable(); } + static void tan(mpq & ) { lean_unreachable(); } + static void sec(mpq & ) { lean_unreachable(); } + static void csc(mpq & ) { lean_unreachable(); } + static void cot(mpq & ) { lean_unreachable(); } + static void asin(mpq & ) { lean_unreachable(); } + static void acos(mpq & ) { lean_unreachable(); } + static void atan(mpq & ) { lean_unreachable(); } + static void sinh(mpq & ) { lean_unreachable(); } + static void cosh(mpq & ) { lean_unreachable(); } + static void tanh(mpq & ) { lean_unreachable(); } + static void asinh(mpq & ) { lean_unreachable(); } + static void acosh(mpq & ) { lean_unreachable(); } + static void atanh(mpq & ) { lean_unreachable(); } }; } diff --git a/src/util/numerics/mpz.h b/src/util/numerics/mpz.h index 8cfd2bc46..e9fe1b347 100644 --- a/src/util/numerics/mpz.h +++ b/src/util/numerics/mpz.h @@ -227,7 +227,7 @@ public: static bool is_zero(mpz const & v) { return v.is_zero(); } static bool is_pos(mpz const & v) { return v.is_pos(); } static bool is_neg(mpz const & v) { return v.is_neg(); } - static void set_rounding(bool plus_inf) {} + static void set_rounding(bool ) {} static void neg(mpz & v) { v.neg(); } static void reset(mpz & v) { v = 0; } // v <- v^k