michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Use consistent coding style for spaces after ','

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-13 12:49:03 -07:00
parent 2c68117adf
commit 8c735f1daa
36 changed files with 269 additions and 269 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/elaborator.cpp
View file

@ -480,7 +480,7 @@ class elaborator::imp {
}
bool is_simple_ho_match(expr const & e1, expr const & e2, context const & ctx) {
if (is_app(e1) && is_meta(arg(e1,0)) && is_var(arg(e1,1), 0) && num_args(e1) == 2 && !is_empty(ctx)) {
if (is_app(e1) && is_meta(arg(e1, 0)) && is_var(arg(e1, 1), 0) && num_args(e1) == 2 && !is_empty(ctx)) {
return true;
} else {
return false;
@ -490,7 +490,7 @@ class elaborator::imp {
void unify_simple_ho_match(expr const & e1, expr const & e2, constraint const & c) {
context const & ctx = c.m_ctx;
context_entry const & head = ::lean::lookup(ctx, 0);
m_constraints.push_back(constraint(arg(e1,0), mk_lambda(head.get_name(),
m_constraints.push_back(constraint(arg(e1, 0), mk_lambda(head.get_name(),
lift_free_vars_mmv(head.get_domain(), 1, 1),
lift_free_vars_mmv(e2, 1, 1)), c));
}
@ -882,7 +882,7 @@ void elaborator::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
void elaborator::clear() { m_ptr->clear(); }
environment const & elaborator::get_environment() const { return m_ptr->get_environment(); }
void elaborator::display(std::ostream & out) const { m_ptr->display(out); }
format elaborator::pp(formatter & f, options const & o) const { return m_ptr->pp(f,o); }
format elaborator::pp(formatter & f, options const & o) const { return m_ptr->pp(f, o); }
void elaborator::print(imp * ptr) { ptr->display(std::cout); }
bool elaborator::has_constraints() const { return m_ptr->has_constraints(); }
}

2
src/frontends/lean/parser.cpp
View file

@ -1423,7 +1423,7 @@ class parser::imp {
<< " Eval [expr] evaluate the given expression" << endl
<< " Help display this message" << endl
<< " Help Options display available options" << endl
<< " Help Notation describe commands for defining infix,mixfix,postfix operators" << endl
<< " Help Notation describe commands for defining infix, mixfix, postfix operators" << endl
<< " Import [string] load the given file" << endl
<< " Set [id] [value] set option [id] with value [value]" << endl
<< " Show [expr] pretty print the given expression" << endl

10
src/frontends/lean/pp.cpp
View file

@ -174,7 +174,7 @@ class pp_fn {
typedef std::pair<format, unsigned> result;
bool is_coercion(expr const & e) {
return is_app(e) && num_args(e) == 2 && m_frontend.is_coercion(arg(e,0));
return is_app(e) && num_args(e) == 2 && m_frontend.is_coercion(arg(e, 0));
}
/**
@ -186,7 +186,7 @@ class pp_fn {
return true;
case expr_kind::App:
if (!m_coercion && is_coercion(e))
return is_atomic(arg(e,1));
return is_atomic(arg(e, 1));
else
return false;
case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Eq: case expr_kind::Let:
@ -490,7 +490,7 @@ class pp_fn {
application(expr const & e, pp_fn const & owner, bool show_implicit):m_app(e) {
frontend const & fe = owner.m_frontend;
expr const & f = arg(e,0);
expr const & f = arg(e, 0);
if (is_constant(f) && owner.has_implicit_arguments(const_name(f))) {
m_implicit_args = &(fe.get_implicit_arguments(const_name(f)));
if (show_implicit || num_args(e) - 1 < m_implicit_args->size()) {
@ -594,7 +594,7 @@ class pp_fn {
*/
result pp_app(expr const & e, unsigned depth) {
if (!m_coercion && is_coercion(e))
return pp(arg(e,1), depth);
return pp(arg(e, 1), depth);
application app(e, *this, m_implict);
operator_info op;
if (m_notation && app.notation_enabled() && (op = get_operator(e)) && has_expected_num_args(app, op)) {
@ -668,7 +668,7 @@ class pp_fn {
} else {
// standard function application
expr const & f = app.get_function();
result p = is_constant(f) && !is_metavar(f) ? mk_result(format(const_name(f)),1) : pp_child(f, depth);
result p = is_constant(f) && !is_metavar(f) ? mk_result(format(const_name(f)), 1) : pp_child(f, depth);
bool simple = is_constant(f) && !is_metavar(f) && const_name(f).size() <= m_indent + 4;
unsigned indent = simple ? const_name(f).size()+1 : m_indent;
format r_format = p.first;

8
src/interval/interval.h
View file

@ -73,18 +73,18 @@ public:
// (-oo, oo)
interval();
// [n,n]
// [n, n]
template<typename T2> interval(T2 const & n):m_lower(n), m_upper(n) { set_closed_endpoints();}
// copy constructor
interval(interval<T> const & n);
// move constructor
interval(interval<T> && src);
// [l,u], (l,u], [l,u), (l,u)
// [l, u], (l, u], [l, u), (l, u)
template<typename T2> interval(T2 const & l, T2 const & u, bool l_open = false, bool u_open = false):m_lower(l), m_upper(u) {
m_lower_open = l_open; m_upper_open = u_open; m_lower_inf = false; m_upper_inf = false;
}
// [l,u], (l,u], [l,u), (l,u)
// [l, u], (l, u], [l, u), (l, u)
template<typename T2> interval(bool l_open, T2 const & l, T2 const & u, bool u_open):interval(l, u, l_open, u_open) {}
// (-oo, u], (-oo, u]
template<typename T2> interval(T2 const & u, bool u_open):m_upper(u) {
@ -129,7 +129,7 @@ public:
bool is_N1() const { return is_upper_neg() || (is_upper_zero() && is_upper_open()); }
// lower is negative and upper is positive
bool is_M() const { return is_lower_neg() && is_upper_pos(); }
// [0,0]
// [0, 0]
bool is_zero() const { return is_lower_zero() && is_upper_zero(); }
// Interval contains the value zero

8
src/interval/interval_def.h
View file

@ -878,7 +878,7 @@ template<typename T> void interval<T>::inv_jst(interval_deps & deps) {
template<typename T>
template<bool compute_intv, bool compute_deps>
void interval<T>::inv(interval_deps & deps) {
// If the interval [l,u] does not contain 0, then 1/[l,u] = [1/u, 1/l]
// If the interval [l, u] does not contain 0, then 1/[l, u] = [1/u, 1/l]
lean_assert(!contains_zero());
using std::swap;
@ -2175,7 +2175,7 @@ void interval<T>::cosh (interval_deps & deps) {
lean_assert(check_invariant());
}
if(compute_deps) {
// cos([a,b]) = [cosh(a), cos(b)]
// cos([a, b]) = [cosh(a), cos(b)]
deps.m_lower_deps = DEP_IN_LOWER1;
deps.m_upper_deps = DEP_IN_LOWER1 | DEP_IN_UPPER1;
}
@ -2197,7 +2197,7 @@ void interval<T>::cosh (interval_deps & deps) {
}
return;
}
// [a,b] where a < 0 < b
// [a, b] where a < 0 < b
if(m_lower + m_upper < 0.0) {
if(compute_intv) {
m_upper = m_lower;
@ -2247,7 +2247,7 @@ void interval<T>::cosh (interval_deps & deps) {
}
}
if(upper_kind() == XN_NUMERAL) {
// [-oo,c]
// [-oo, c]
lean_assert(lower_kind() == XN_MINUS_INFINITY);
if(compute_intv) {
m_upper_inf = true;

6
src/kernel/builtin.cpp
View file

@ -204,10 +204,10 @@ void import_basic(environment & env) {
// forall : Pi (A : Type u), (A -> Bool) -> Bool
env.add_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True))));
// TODO(Leo): introduce epsilon
env.add_definition(exists_fn_name, q_type, Fun({{A,TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
env.add_definition(exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
// homogeneous equality
env.add_definition(homo_eq_fn_name, Pi({{A,TypeU},{x,A},{y,A}}, Bool), Fun({{A,TypeU}, {x,A}, {y,A}}, Eq(x, y)));
env.add_definition(homo_eq_fn_name, Pi({{A, TypeU}, {x, A}, {y, A}}, Bool), Fun({{A, TypeU}, {x, A}, {y, A}}, Eq(x, y)));
// MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b
env.add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b));
@ -222,7 +222,7 @@ void import_basic(environment & env) {
env.add_axiom(case_fn_name, Pi({{P, Bool >> Bool}, {H1, P(True)}, {H2, P(False)}, {a, Bool}}, P(a)));
// Subst : Pi (A : Type u) (a b : A) (P : A -> bool) (H1 : P a) (H2 : a = b), P b
env.add_axiom(subst_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {P, A_pred}, {H1, P(a)}, {H2, Eq(a,b)}}, P(b)));
env.add_axiom(subst_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {P, A_pred}, {H1, P(a)}, {H2, Eq(a, b)}}, P(b)));
// Eta : Pi (A : Type u) (B : A -> Type u), f : (Pi x : A, B x), (Fun x : A => f x) = f
env.add_axiom(eta_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}}, Eq(Fun({x, A}, f(x)), f)));

4
src/kernel/context.h
View file

@ -34,8 +34,8 @@ class context {
explicit context(list<context_entry> const & l):m_list(l) {}
public:
context() {}
context(context const & c, name const & n, expr const & d):m_list(context_entry(n,d), c.m_list) {}
context(context const & c, name const & n, expr const & d, expr const & b):m_list(context_entry(n,d,b), c.m_list) {}
context(context const & c, name const & n, expr const & d):m_list(context_entry(n, d), c.m_list) {}
context(context const & c, name const & n, expr const & d, expr const & b):m_list(context_entry(n, d, b), c.m_list) {}
context_entry const & lookup(unsigned vidx) const;
std::pair<context_entry const &, context> lookup_ext(unsigned vidx) const;
bool is_empty() const { return is_nil(m_list); }

6
src/kernel/expr.h
View file

@ -30,7 +30,7 @@ class value;
| Eq expr expr (heterogeneous equality)
| Let name expr expr expr
TODO: match expressions.
TODO(Leo): match expressions.
The main API is divided in the following sections
- Testers
@ -386,11 +386,11 @@ struct expr_eqp { bool operator()(expr const & e1, expr const & e2) const { retu
struct expr_cell_hash { unsigned operator()(expr_cell * e) const { return e->hash(); } };
/** \brief Functional object for testing pointer equality between kernel cell expressions. */
struct expr_cell_eqp { bool operator()(expr_cell * e1, expr_cell * e2) const { return e1 == e2; } };
/** \brief Functional object for hashing a pair (n,k) where n is a kernel expressions, and k is an offset. */
/** \brief Functional object for hashing a pair (n, k) where n is a kernel expressions, and k is an offset. */
struct expr_offset_hash { unsigned operator()(expr_offset const & p) const { return hash(p.first.hash(), p.second); } };
/** \brief Functional object for comparing pairs (expression, offset). */
struct expr_offset_eqp { unsigned operator()(expr_offset const & p1, expr_offset const & p2) const { return is_eqp(p1.first, p2.first) && p1.second == p2.second; } };
/** \brief Functional object for hashing a pair (n,k) where n is a kernel cell expressions, and k is an offset. */
/** \brief Functional object for hashing a pair (n, k) where n is a kernel cell expressions, and k is an offset. */
struct expr_cell_offset_hash { unsigned operator()(expr_cell_offset const & p) const { return hash(p.first->hash(), p.second); } };
/** \brief Functional object for comparing pairs (expression cell, offset). */
struct expr_cell_offset_eqp { unsigned operator()(expr_cell_offset const & p1, expr_cell_offset const & p2) const { return p1 == p2; } };

4
src/kernel/instantiate.h
View file

@ -9,7 +9,7 @@ Author: Leonardo de Moura
namespace lean {
/**
\brief Replace the free variables with indices 0,...,n-1 with s[n-1],...,s[0] in e.
\brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e.
\pre s[0], ..., s[n-1] must be closed expressions (i.e., no free variables).
*/
@ -17,7 +17,7 @@ expr instantiate_with_closed(expr const & e, unsigned n, expr const * s);
inline expr instantiate_with_closed(expr const & e, expr const & s) { return instantiate_with_closed(e, 1, &s); }
/**
\brief Replace the free variables with indices 0,...,n-1 with s[n-1],...,s[0] in e.
\brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e.
*/
expr instantiate(expr const & e, unsigned n, expr const * s);
inline expr instantiate(expr const & e, expr const & s) { return instantiate(e, 1, &s); }

18
src/library/arith/special_fn.cpp
View file

@ -42,19 +42,19 @@ void import_special_fn(environment & env) {
env.add_var(real_pi_name, Real);
env.add_definition(name("pi"), Real, mk_real_pi()); // alias for pi
env.add_var(sin_fn_name, r_r);
env.add_definition(cos_fn_name, r_r, Fun({x,Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2))))));
env.add_definition(tan_fn_name, r_r, Fun({x,Real}, rDiv(Sin(x), Cos(x))));
env.add_definition(cot_fn_name, r_r, Fun({x,Real}, rDiv(Cos(x), Sin(x))));
env.add_definition(sec_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Cos(x))));
env.add_definition(csc_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Sin(x))));
env.add_definition(cos_fn_name, r_r, Fun({x, Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2))))));
env.add_definition(tan_fn_name, r_r, Fun({x, Real}, rDiv(Sin(x), Cos(x))));
env.add_definition(cot_fn_name, r_r, Fun({x, Real}, rDiv(Cos(x), Sin(x))));
env.add_definition(sec_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cos(x))));
env.add_definition(csc_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sin(x))));
env.add_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))),
rMul(rVal(2), Exp(rNeg(x))))));
env.add_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))),
rMul(rVal(2), Exp(rNeg(x))))));
env.add_definition(tanh_fn_name, r_r, Fun({x,Real}, rDiv(Sinh(x), Cosh(x))));
env.add_definition(coth_fn_name, r_r, Fun({x,Real}, rDiv(Cosh(x), Sinh(x))));
env.add_definition(sech_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Cosh(x))));
env.add_definition(csch_fn_name, r_r, Fun({x,Real}, rDiv(rVal(1), Sinh(x))));
env.add_definition(tanh_fn_name, r_r, Fun({x, Real}, rDiv(Sinh(x), Cosh(x))));
env.add_definition(coth_fn_name, r_r, Fun({x, Real}, rDiv(Cosh(x), Sinh(x))));
env.add_definition(sech_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cosh(x))));
env.add_definition(csch_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sinh(x))));
}
}

10
src/library/basic_thms.cpp
View file

@ -184,9 +184,9 @@ void import_basic_thms(environment & env) {
Discharge(Not(b), a, Fun({H1, Not(b)},
FalseElim(a, Absurd(b, H, H1))))))));
// DisjCases : Pi (a b c: Bool) (H1 : Or(a,b)) (H2 : a -> c) (H3 : b -> c), c */
env.add_theorem(disj_cases_fn_name, Pi({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a,b)}, {H2, a >> c}, {H3, b >> c}}, c),
Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a,b)}, {H2, a >> c}, {H3, b >> c}},
// DisjCases : Pi (a b c: Bool) (H1 : Or(a, b)) (H2 : a -> c) (H3 : b -> c), c */
env.add_theorem(disj_cases_fn_name, Pi({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}}, c),
Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}},
EqMP(Not(Not(c)), c, DoubleNeg(c),
Discharge(Not(c), False,
Fun({H, Not(c)},
@ -200,11 +200,11 @@ void import_basic_thms(environment & env) {
// Symm : Pi (A : Type u) (a b : A) (H : a = b), b = a
env.add_theorem(symm_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, Eq(b, a)),
Fun({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}},
Subst(A, a, b, Fun({x, A}, Eq(x,a)), Refl(A, a), H)));
Subst(A, a, b, Fun({x, A}, Eq(x, a)), Refl(A, a), H)));
// Trans: Pi (A: Type u) (a b c : A) (H1 : a = b) (H2 : b = c), a = c
env.add_theorem(trans_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)),
Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a,b)}, {H2, Eq(b,c)}},
Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}},
Subst(A, b, c, Fun({x, A}, Eq(a, x)), H1, H2)));
// TransExt: Pi (A: Type u) (B : Type u) (a : A) (b c : B) (H1 : a = b) (H2 : b = c), a = c

2
src/library/basic_thms.h
View file

@ -81,7 +81,7 @@ expr mk_disj2_fn();
inline expr Disj2(expr const & b, expr const & a, expr const & H) { return mk_app(mk_disj2_fn(), b, a, H); }
expr mk_disj_cases_fn();
/** \brief (Theorem) {a b c : Bool}, H1 : Or(a,b), H2 : a -> c, H3 : b -> c |- DisjCases(a, b, c, H1, H2, H3) : c */
/** \brief (Theorem) {a b c : Bool}, H1 : Or(a, b), H2 : a -> c, H3 : b -> c |- DisjCases(a, b, c, H1, H2, H3) : c */
inline expr DisjCases(expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2, expr const & H3) { return mk_app({mk_disj_cases_fn(), a, b, c, H1, H2, H3}); }
expr mk_symm_fn();

4
src/library/cast/cast.cpp
View file

@ -22,7 +22,7 @@ public:
expr A = Const("A");
expr B = Const("B");
// Cast: Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B
m_type = Pi({{A, TypeU}, {B, TypeU}}, Eq(A,B) >> (A >> B));
m_type = Pi({{A, TypeU}, {B, TypeU}}, Eq(A, B) >> (A >> B));
}
virtual ~cast_fn_value() {}
virtual expr get_type() const { return m_type; }
@ -122,7 +122,7 @@ void import_cast(environment & env) {
// Alias for Cast operator. We create the alias to be able to mark
// implicit arguments.
env.add_definition(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}}, Eq(A,B) >> (A >> B)), mk_Cast_fn());
env.add_definition(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}}, Eq(A, B) >> (A >> B)), mk_Cast_fn());
// DomInj : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A'
env.add_axiom(dom_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}}, Eq(A, Ap)));

2
src/library/context_to_lambda.cpp
View file

@ -25,7 +25,7 @@ expr context_to_lambda(context const & c, expr const & e) {
return context_to_lambda(c.begin(), c.end(), e);
}
bool is_fake_context(expr const & e) {
return is_lambda(e) && is_app(abst_domain(e)) && arg(abst_domain(e),0) == g_fake;
return is_lambda(e) && is_app(abst_domain(e)) && arg(abst_domain(e), 0) == g_fake;
}
name const & fake_context_name(expr const & e) {
lean_assert(is_fake_context(e));

2
src/library/formatter.cpp
View file

@ -22,7 +22,7 @@ public:
std::ostringstream s;
if (format_ctx)
s << c << "|-\n";
s << mk_pair(e,c);
s << mk_pair(e, c);
return format(s.str());
}
virtual format operator()(object const & obj, options const & opts) {

6
src/library/metavar.cpp
View file

@ -319,11 +319,11 @@ static expr get_def_value(name const & n, environment const & env, name_set cons
expr head_reduce_mmv(expr const & e, environment const & env, name_set const * defs) {
if (is_app(e) && is_lambda(arg(e, 0))) {
expr r = arg(e,0);
expr r = arg(e, 0);
unsigned num = num_args(e);
unsigned i = 1;
while (i < num) {
r = instantiate_free_var_mmv(abst_body(r), 0, arg(e,i));
r = instantiate_free_var_mmv(abst_body(r), 0, arg(e, i));
i = i + 1;
if (!is_lambda(r))
break;
@ -332,7 +332,7 @@ expr head_reduce_mmv(expr const & e, environment const & env, name_set const * d
buffer<expr> args;
args.push_back(r);
for (; i < num; i++)
args.push_back(arg(e,i));
args.push_back(arg(e, i));
r = mk_app(args.size(), args.data());
}
return r;

160
src/tests/frontends/lean/implicit_args.cpp
View file

@ -81,9 +81,9 @@ static void tst1() {
env.add_var("F", Pi({{A, Type()}, {B, Type()}, {g, A >> B}}, A));
env.add_var("f", Nat >> Real);
expr f = Const("f");
success(F(_,_,f), F(Nat, Real, f), env);
// fails(F(_,Bool,f), env);
success(F(_,_,Fun({a, Nat},a)), F(Nat,Nat,Fun({a,Nat},a)), env);
success(F(_, _, f), F(Nat, Real, f), env);
// fails(F(_, Bool, f), env);
success(F(_, _, Fun({a, Nat}, a)), F(Nat, Nat, Fun({a, Nat}, a)), env);
}
static void tst2() {
@ -98,15 +98,15 @@ static void tst2() {
env.add_var("c", Bool);
env.add_axiom("H1", Eq(a, b));
env.add_axiom("H2", Eq(b, c));
success(Trans(_,_,_,_,H1,H2), Trans(Bool,a,b,c,H1,H2), env);
success(Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1)),
Trans(Bool,c,b,a,Symm(Bool,b,c,H2),Symm(Bool,a,b,H1)), env);
success(Symm(_,_,_,Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1))),
Symm(Bool,c,a,Trans(Bool,c,b,a,Symm(Bool,b,c,H2),Symm(Bool,a,b,H1))), env);
success(Trans(_, _, _, _, H1, H2), Trans(Bool, a, b, c, H1, H2), env);
success(Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1)),
Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1)), env);
success(Symm(_, _, _, Trans(_, _ , _ , _ , Symm(_, _, _, H2), Symm(_, _, _, H1))),
Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), env);
env.add_axiom("H3", a);
expr H3 = Const("H3");
success(EqTIntro(_, EqMP(_,_,Symm(_,_,_,Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1))), H3)),
EqTIntro(c, EqMP(a,c,Symm(Bool,c,a,Trans(Bool,c,b,a,Symm(Bool,b,c,H2),Symm(Bool,a,b,H1))), H3)),
success(EqTIntro(_, EqMP(_, _, Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1))), H3)),
EqTIntro(c, EqMP(a, c, Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), H3)),
env);
}
@ -127,17 +127,17 @@ static void tst3() {
env.add_var("b", Nat);
env.add_definition("fact", Bool, Eq(a, b));
env.add_axiom("H", fact);
success(Congr2(_,_,_,_,f,H),
Congr2(Nat, Fun({n,Nat}, vec(n) >> Nat), a, b, f, H), env);
success(Congr2(_, _, _, _, f, H),
Congr2(Nat, Fun({n, Nat}, vec(n) >> Nat), a, b, f, H), env);
env.add_var("g", Pi({n, Nat}, vec(n) >> Nat));
expr g = Const("g");
env.add_axiom("H2", Eq(f, g));
expr H2 = Const("H2");
success(Congr(_,_,_,_,_,_,H2,H),
Congr(Nat, Fun({n,Nat}, vec(n) >> Nat), f, g, a, b, H2, H), env);
success(Congr(_,_,_,_,_,_,Refl(_,f),H),
Congr(Nat, Fun({n,Nat}, vec(n) >> Nat), f, f, a, b, Refl(Pi({n, Nat}, vec(n) >> Nat),f), H), env);
success(Refl(_,a), Refl(Nat,a), env);
success(Congr(_, _, _, _, _, _, H2, H),
Congr(Nat, Fun({n, Nat}, vec(n) >> Nat), f, g, a, b, H2, H), env);
success(Congr(_, _, _, _, _, _, Refl(_, f), H),
Congr(Nat, Fun({n, Nat}, vec(n) >> Nat), f, f, a, b, Refl(Pi({n, Nat}, vec(n) >> Nat), f), H), env);
success(Refl(_, a), Refl(Nat, a), env);
}
static void tst4() {
@ -153,13 +153,13 @@ static void tst4() {
expr x = Const("x");
expr y = Const("y");
expr z = Const("z");
success(Fun({{x,_},{y,_}}, f(x, y)),
Fun({{x,Nat},{y,R >> Nat}}, f(x, y)), env);
success(Fun({{x,_},{y,_},{z,_}}, Eq(f(x, y), f(x, z))),
Fun({{x,Nat},{y,R >> Nat},{z,R >> Nat}}, Eq(f(x, y), f(x, z))), env);
success(Fun({{x, _}, {y, _}}, f(x, y)),
Fun({{x, Nat}, {y, R >> Nat}}, f(x, y)), env);
success(Fun({{x, _}, {y, _}, {z, _}}, Eq(f(x, y), f(x, z))),
Fun({{x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, Eq(f(x, y), f(x, z))), env);
expr A = Const("A");
success(Fun({{A,Type()},{x,_},{y,_},{z,_}}, Eq(f(x, y), f(x, z))),
Fun({{A,Type()},{x,Nat},{y,R >> Nat},{z,R >> Nat}}, Eq(f(x, y), f(x, z))), env);
success(Fun({{A, Type()}, {x, _}, {y, _}, {z, _}}, Eq(f(x, y), f(x, z))),
Fun({{A, Type()}, {x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, Eq(f(x, y), f(x, z))), env);
}
static void tst5() {
@ -172,10 +172,10 @@ static void tst5() {
expr g = Const("g");
expr Nat = Const("N");
env.add_var("N", Type());
env.add_var("f", Pi({{A,Type()},{a,A},{b,A}}, A));
env.add_var("f", Pi({{A, Type()}, {a, A}, {b, A}}, A));
env.add_var("g", Nat >> Nat);
success(Fun({{a,_},{b,_}},g(f(_,a,b))),
Fun({{a,Nat},{b,Nat}},g(f(Nat,a,b))), env);
success(Fun({{a, _}, {b, _}}, g(f(_, a, b))),
Fun({{a, Nat}, {b, Nat}}, g(f(Nat, a, b))), env);
}
static void tst6() {
@ -193,14 +193,14 @@ static void tst6() {
env.add_var("nil", Pi({A, Type()}, lst(A)));
env.add_var("cons", Pi({{A, Type()}, {a, A}, {l, lst(A)}}, lst(A)));
env.add_var("f", lst(N>>N) >> Bool);
success(Fun({a,_}, f(cons(_, a, cons(_, a, nil(_))))),
Fun({a,N>>N}, f(cons(N>>N, a, cons(N>>N, a, nil(N>>N))))), env);
success(Fun({a, _}, f(cons(_, a, cons(_, a, nil(_))))),
Fun({a, N>>N}, f(cons(N>>N, a, cons(N>>N, a, nil(N>>N))))), env);
}
static void tst7() {
frontend env;
expr x = Const("x");
expr omega = mk_app(Fun({x,_}, x(x)), Fun({x,_}, x(x)));
expr omega = mk_app(Fun({x, _}, x(x)), Fun({x, _}, x(x)));
fails(omega, env);
}
@ -211,18 +211,18 @@ static void tst8() {
expr x = Const("x");
expr f = Const("f");
env.add_var("f", Pi({B, Type()}, B >> B));
success(Fun({{A,Type()}, {B,Type()}, {x,_}}, f(B, x)),
Fun({{A,Type()}, {B,Type()}, {x,B}}, f(B, x)), env);
fails(Fun({{x,_}, {A,Type()}}, f(A, x)), env);
success(Fun({{A,Type()}, {x,_}}, f(A, x)),
Fun({{A,Type()}, {x,A}}, f(A, x)), env);
success(Fun({{A,Type()}, {B,Type()}, {x,_}}, f(A, x)),
Fun({{A,Type()}, {B,Type()}, {x,A}}, f(A, x)), env);
success(Fun({{A,Type()}, {B,Type()}, {x,_}}, Eq(f(B, x), f(_,x))),
Fun({{A,Type()}, {B,Type()}, {x,B}}, Eq(f(B, x), f(B,x))), env);
success(Fun({{A,Type()}, {B,_}, {x,_}}, Eq(f(B, x), f(_,x))),
Fun({{A,Type()}, {B,Type()}, {x,B}}, Eq(f(B, x), f(B,x))), env);
unsolved(Fun({{A,_}, {B,_}, {x,_}}, Eq(f(B, x), f(_,x))), env);
success(Fun({{A, Type()}, {B, Type()}, {x, _}}, f(B, x)),
Fun({{A, Type()}, {B, Type()}, {x, B}}, f(B, x)), env);
fails(Fun({{x, _}, {A, Type()}}, f(A, x)), env);
success(Fun({{A, Type()}, {x, _}}, f(A, x)),
Fun({{A, Type()}, {x, A}}, f(A, x)), env);
success(Fun({{A, Type()}, {B, Type()}, {x, _}}, f(A, x)),
Fun({{A, Type()}, {B, Type()}, {x, A}}, f(A, x)), env);
success(Fun({{A, Type()}, {B, Type()}, {x, _}}, Eq(f(B, x), f(_, x))),
Fun({{A, Type()}, {B, Type()}, {x, B}}, Eq(f(B, x), f(B, x))), env);
success(Fun({{A, Type()}, {B, _}, {x, _}}, Eq(f(B, x), f(_, x))),
Fun({{A, Type()}, {B, Type()}, {x, B}}, Eq(f(B, x), f(B, x))), env);
unsolved(Fun({{A, _}, {B, _}, {x, _}}, Eq(f(B, x), f(_, x))), env);
}
static void tst9() {
@ -234,7 +234,7 @@ static void tst9() {
expr x = Const("x");
expr y = Const("y");
env.add_var("N", Type());
env.add_var("f", Pi({A,Type()}, A >> A));
env.add_var("f", Pi({A, Type()}, A >> A));
expr N = Const("N");
success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))}, g(_, True, False)),
Fun({g, Pi({A, Type()}, A >> (A >> Bool))}, g(Bool, True, False)),
@ -247,21 +247,21 @@ static void tst9() {
env);
success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
g(_,
Fun({{x,_},{y,_}}, Eq(f(_, x), f(_, y))),
Fun({{x,N},{y,Bool}}, True))),
Fun({{x, _}, {y, _}}, Eq(f(_, x), f(_, y))),
Fun({{x, N}, {y, Bool}}, True))),
Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
g((N >> (Bool >> Bool)),
Fun({{x,N},{y,Bool}}, Eq(f(N, x), f(Bool, y))),
Fun({{x,N},{y,Bool}}, True))), env);
Fun({{x, N}, {y, Bool}}, Eq(f(N, x), f(Bool, y))),
Fun({{x, N}, {y, Bool}}, True))), env);
success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
g(_,
Fun({{x,N},{y,_}}, Eq(f(_, x), f(_, y))),
Fun({{x,_},{y,Bool}}, True))),
Fun({{x, N}, {y, _}}, Eq(f(_, x), f(_, y))),
Fun({{x, _}, {y, Bool}}, True))),
Fun({g, Pi({A, Type()}, A >> (A >> Bool))},
g((N >> (Bool >> Bool)),
Fun({{x,N},{y,Bool}}, Eq(f(N, x), f(Bool, y))),
Fun({{x,N},{y,Bool}}, True))), env);
Fun({{x, N}, {y, Bool}}, Eq(f(N, x), f(Bool, y))),
Fun({{x, N}, {y, Bool}}, True))), env);
}
static void tst10() {
@ -273,19 +273,19 @@ static void tst10() {
expr b = Const("b");
expr eq = Const("eq");
env.add_var("eq", Pi({A, Type()}, A >> (A >> Bool)));
success(Fun({{A, Type()},{B,Type()},{a,_},{b,B}}, eq(_,a,b)),
Fun({{A, Type()},{B,Type()},{a,B},{b,B}}, eq(B,a,b)), env);
success(Fun({{A, Type()},{B,Type()},{a,_},{b,A}}, eq(_,a,b)),
Fun({{A, Type()},{B,Type()},{a,A},{b,A}}, eq(A,a,b)), env);
success(Fun({{A, Type()},{B,Type()},{a,A},{b,_}}, eq(_,a,b)),
Fun({{A, Type()},{B,Type()},{a,A},{b,A}}, eq(A,a,b)), env);
success(Fun({{A, Type()},{B,Type()},{a,B},{b,_}}, eq(_,a,b)),
Fun({{A, Type()},{B,Type()},{a,B},{b,B}}, eq(B,a,b)), env);
success(Fun({{A, Type()},{B,Type()},{a,B},{b,_},{C,Type()}}, eq(_,a,b)),
Fun({{A, Type()},{B,Type()},{a,B},{b,B},{C,Type()}}, eq(B,a,b)), env);
fails(Fun({{A, Type()},{B,Type()},{a,_},{b,_},{C,Type()}}, eq(C,a,b)), env);
success(Fun({{A, Type()},{B,Type()},{a,_},{b,_},{C,Type()}}, eq(B,a,b)),
Fun({{A, Type()},{B,Type()},{a,B},{b,B},{C,Type()}}, eq(B,a,b)), env);
success(Fun({{A, Type()}, {B, Type()}, {a, _}, {b, B}}, eq(_, a, b)),
Fun({{A, Type()}, {B, Type()}, {a, B}, {b, B}}, eq(B, a, b)), env);
success(Fun({{A, Type()}, {B, Type()}, {a, _}, {b, A}}, eq(_, a, b)),
Fun({{A, Type()}, {B, Type()}, {a, A}, {b, A}}, eq(A, a, b)), env);
success(Fun({{A, Type()}, {B, Type()}, {a, A}, {b, _}}, eq(_, a, b)),
Fun({{A, Type()}, {B, Type()}, {a, A}, {b, A}}, eq(A, a, b)), env);
success(Fun({{A, Type()}, {B, Type()}, {a, B}, {b, _}}, eq(_, a, b)),
Fun({{A, Type()}, {B, Type()}, {a, B}, {b, B}}, eq(B, a, b)), env);
success(Fun({{A, Type()}, {B, Type()}, {a, B}, {b, _}, {C, Type()}}, eq(_, a, b)),
Fun({{A, Type()}, {B, Type()}, {a, B}, {b, B}, {C, Type()}}, eq(B, a, b)), env);
fails(Fun({{A, Type()}, {B, Type()}, {a, _}, {b, _}, {C, Type()}}, eq(C, a, b)), env);
success(Fun({{A, Type()}, {B, Type()}, {a, _}, {b, _}, {C, Type()}}, eq(B, a, b)),
Fun({{A, Type()}, {B, Type()}, {a, B}, {b, B}, {C, Type()}}, eq(B, a, b)), env);
}
@ -299,28 +299,28 @@ static void tst11() {
env.add_var("a", Bool);
env.add_var("b", Bool);
env.add_var("c", Bool);
success(Fun({{H1, Eq(a,b)},{H2,Eq(b,c)}},
Trans(_,_,_,_,H1,H2)),
Fun({{H1, Eq(a,b)},{H2,Eq(b,c)}},
Trans(Bool,a,b,c,H1,H2)),
success(Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}},
Trans(_, _, _, _, H1, H2)),
Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}},
Trans(Bool, a, b, c, H1, H2)),
env);
expr H3 = Const("H3");
success(Fun({{H1, Eq(a,b)},{H2,Eq(b,c)},{H3,a}},
EqTIntro(_, EqMP(_,_,Symm(_,_,_,Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1))), H3))),
Fun({{H1, Eq(a,b)},{H2,Eq(b,c)},{H3,a}},
EqTIntro(c, EqMP(a,c,Symm(Bool,c,a,Trans(Bool,c,b,a,Symm(Bool,b,c,H2),Symm(Bool,a,b,H1))), H3))),
success(Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}},
EqTIntro(_, EqMP(_, _, Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1))), H3))),
Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}},
EqTIntro(c, EqMP(a, c, Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), H3))),
env);
frontend env2;
success(Fun({{a,Bool},{b,Bool},{c,Bool},{H1, Eq(a,b)},{H2,Eq(b,c)},{H3,a}},
EqTIntro(_, EqMP(_,_,Symm(_,_,_,Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1))), H3))),
Fun({{a,Bool},{b,Bool},{c,Bool},{H1, Eq(a,b)},{H2,Eq(b,c)},{H3,a}},
EqTIntro(c, EqMP(a,c,Symm(Bool,c,a,Trans(Bool,c,b,a,Symm(Bool,b,c,H2),Symm(Bool,a,b,H1))), H3))),
success(Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}},
EqTIntro(_, EqMP(_, _, Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1))), H3))),
Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Eq(a, b)}, {H2, Eq(b, c)}, {H3, a}},
EqTIntro(c, EqMP(a, c, Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), H3))),
env2);
expr A = Const("A");
success(Fun({{A,Type()},{a,A},{b,A},{c,A},{H1, Eq(a,b)},{H2,Eq(b,c)}},
Symm(_,_,_,Trans(_,_,_,_,Symm(_,_,_,H2),Symm(_,_,_,H1)))),
Fun({{A,Type()},{a,A},{b,A},{c,A},{H1, Eq(a,b)},{H2,Eq(b,c)}},
Symm(A,c,a,Trans(A,c,b,a,Symm(A,b,c,H2),Symm(A,a,b,H1)))),
success(Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}},
Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1)))),
Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}},
Symm(A, c, a, Trans(A, c, b, a, Symm(A, b, c, H2), Symm(A, a, b, H1)))),
env2);
}
@ -360,7 +360,7 @@ void tst14() {
expr h = Const("h");
expr D = Const("D");
env.add_var("R", Type() >> Bool);
env.add_var("r", Pi({A, Type()},R(A)));
env.add_var("r", Pi({A, Type()}, R(A)));
env.add_var("h", Pi({A, Type()}, R(A)) >> Bool);
env.add_var("eq", Pi({A, Type(level()+1)}, A >> (A >> Bool)));
success(Let({{f, Fun({A, Type()}, r(_))},

4
src/tests/frontends/lean/lean_frontend.cpp
View file

@ -159,7 +159,7 @@ static void tst10() {
expr x = Const("xxxxxxxxxxxx");
expr y = Const("y");
expr z = Const("foo");
expr e = Let({{x, True}, {y, And({x,x,x,x,x,x,x,x})}, {z, And(x, y)}}, Or({x, x, x, x, x, x, x, x, x, z, z, z, z, z, z, z}));
expr e = Let({{x, True}, {y, And({x, x, x, x, x, x, x, x})}, {z, And(x, y)}}, Or({x, x, x, x, x, x, x, x, x, z, z, z, z, z, z, z}));
std::cout << e << "\n";
std::cout << fmt(e) << "\n";
}
@ -188,7 +188,7 @@ static void tst11() {
} catch (exception & ex) {
std::cout << "Expected error: " << ex.what() << std::endl;
}
f.add_var(name{"h","explicit"}, Pi({A, Type()}, A >> (A >> A)));
f.add_var(name{"h", "explicit"}, Pi({A, Type()}, A >> (A >> A)));
f.add_var("h", Pi({A, Type()}, A >> (A >> A)));
try {
f.mark_implicit_arguments("h", {true, false, false});

6
src/tests/interval/interval.cpp
View file

@ -84,10 +84,10 @@ static void tst2() {
lean_assert(power(qi(-3, -2), 2) == qi(4, 9));
std::cout << power(qi(false, -3, -2, true), 2) << " --> " << qi(true, 4, 9, false) << "\n";
lean_assert(power(qi(false, -3, -2, true), 2) == qi(true, 4, 9, false));
lean_assert(power(qi(-3,-1), 3) == qi(-27, -1));
lean_assert(power(qi(-3, -1), 3) == qi(-27, -1));
lean_assert(power(qi(-3, 4), 3) == qi(-27, 64));
lean_assert(power(qi(),3) == qi());
lean_assert(power(qi(),2) == qi(false, 0)); // (-oo, oo)^2 == [0, oo)
lean_assert(power(qi(), 3) == qi());
lean_assert(power(qi(), 2) == qi(false, 0)); // (-oo, oo)^2 == [0, oo)
}
int main() {

12
src/tests/kernel/expr.cpp
View file

@ -224,8 +224,8 @@ void tst6() {
void tst7() {
expr f = Const("f");
expr v = Var(0);
expr a1 = max_sharing(f(v,v));
expr a2 = max_sharing(f(v,v));
expr a1 = max_sharing(f(v, v));
expr a2 = max_sharing(f(v, v));
lean_assert(!is_eqp(a1, a2));
expr b = max_sharing(f(a1, a2));
lean_assert(is_eqp(arg(b, 1), arg(b, 2)));
@ -315,7 +315,7 @@ void tst12() {
expr a = Const("a");
expr x = Var(0);
expr t = Type();
expr F = mk_pi("y", t, mk_lambda("x", t, f(f(f(x,a),Const("10")),x)));
expr F = mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), x)));
expr G = deep_copy(F);
lean_assert(F == G);
lean_assert(!is_eqp(F, G));
@ -325,12 +325,12 @@ void tst12() {
void tst13() {
expr f = Const("f");
expr v = Var(0);
expr a1 = max_sharing(f(v,v));
expr a2 = max_sharing(f(v,v));
expr a1 = max_sharing(f(v, v));
expr a2 = max_sharing(f(v, v));
lean_assert(!is_eqp(a1, a2));
lean_assert(a1 == a2);
max_sharing_fn M;
lean_assert(is_eqp(M(f(v,v)), M(f(v,v))));
lean_assert(is_eqp(M(f(v, v)), M(f(v, v))));
lean_assert(is_eqp(M(a1), M(a2)));
}

10
src/tests/kernel/normalizer.cpp
View file

@ -157,9 +157,9 @@ static void tst2() {
expr h = Const("h");
expr x = Var(0);
expr y = Var(1);
lean_assert(normalize(f(x,x), env, extend(context(), name("f"), t, f(a))) == f(f(a), f(a)));
lean_assert(normalize(f(x, x), env, extend(context(), name("f"), t, f(a))) == f(f(a), f(a)));
context c1 = extend(extend(context(), name("f"), t, f(a)), name("h"), t, h(x));
expr F1 = normalize(f(x,f(x)), env, c1);
expr F1 = normalize(f(x, f(x)), env, c1);
lean_assert(F1 == f(h(f(a)), f(h(f(a)))));
std::cout << F1 << "\n";
expr F2 = normalize(mk_lambda("x", t, f(x, f(y))), env, c1);
@ -168,10 +168,10 @@ static void tst2() {
expr F3 = normalize(mk_lambda("y", t, mk_lambda("x", t, f(x, f(y)))), env, c1);
std::cout << F3 << "\n";
lean_assert(F3 == mk_lambda("y", t, mk_lambda("x", t, f(x, f(y)))));
context c2 = extend(extend(context(), name("foo"), t, mk_lambda("x", t, f(x, a))), name("bla"), t, mk_lambda("z", t, h(x,y)));
context c2 = extend(extend(context(), name("foo"), t, mk_lambda("x", t, f(x, a))), name("bla"), t, mk_lambda("z", t, h(x, y)));
expr F4 = normalize(mk_lambda("x", t, f(x, f(y))), env, c2);
std::cout << F4 << "\n";
lean_assert(F4 == mk_lambda("x", t, f(x, f(mk_lambda("z", t, h(x,mk_lambda("x", t, f(x, a))))))));
lean_assert(F4 == mk_lambda("x", t, f(x, f(mk_lambda("z", t, h(x, mk_lambda("x", t, f(x, a))))))));
context c3 = extend(context(), name("x"), t);
expr f5 = mk_app(mk_lambda("f", t, mk_lambda("z", t, Var(1))), mk_lambda("y", t, Var(1)));
expr F5 = normalize(f5, env, c3);
@ -180,7 +180,7 @@ static void tst2() {
lean_assert(F5 == mk_lambda("z", t, mk_lambda("y", t, Var(2))));
context c4 = extend(extend(context(), name("x"), t), name("x2"), t);
expr F6 = normalize(mk_app(mk_lambda("f", t, mk_lambda("z1", t, mk_lambda("z2", t, mk_app(Var(2), Const("a"))))),
mk_lambda("y", t, mk_app(Var(1), Var(2), Var(0)))), env, c4);
mk_lambda("y", t, mk_app(Var(1), Var(2), Var(0)))), env, c4);
std::cout << F6 << "\n";
lean_assert(F6 == mk_lambda("z1", t, mk_lambda("z2", t, mk_app(Var(2), Var(3), Const("a")))));
}

6
src/tests/kernel/replace.cpp
View file

@ -80,17 +80,17 @@ static void tst3() {
}
};
replace_fn<decltype(proc), tracer> replacer(proc, tracer(trace));
expr t = Fun({{x, A}, {y, A}}, f(x, f(f(f(x,x), f(y, d)), f(d, d))));
expr t = Fun({{x, A}, {y, A}}, f(x, f(f(f(x, x), f(y, d)), f(d, d))));
expr b = abst_body(t);
expr r = replacer(b);
std::cout << r << "\n";
lean_assert(r == Fun({y, A}, f(c, f(f(f(c,c), f(y, d)), f(d, d)))));
lean_assert(r == Fun({y, A}, f(c, f(f(f(c, c), f(y, d)), f(d, d)))));
for (auto p : trace) {
std::cout << p.first << " --> " << p.second << "\n";
}
lean_assert(trace[c] == Var(1));
std::cout << arg(arg(abst_body(r), 2), 2) << "\n";
lean_assert(arg(arg(abst_body(r), 2), 2) == f(d,d));
lean_assert(arg(arg(abst_body(r), 2), 2) == f(d, d));
lean_assert(trace.find(arg(arg(abst_body(r), 2), 2)) == trace.end());
lean_assert(trace.find(abst_body(r)) != trace.end());
lean_assert(trace.find(arg(abst_body(r), 2)) != trace.end());

16
src/tests/kernel/type_checker.cpp
View file

@ -194,18 +194,18 @@ static void tst11() {
unsigned n = 1000;
expr f = Const("f");
expr a = Const("a");
expr t1 = f(a,a);
expr t1 = f(a, a);
expr b = Const("a");
expr t2 = f(a,a);
expr t3 = f(b,b);
expr t2 = f(a, a);
expr t3 = f(b, b);
for (unsigned i = 0; i < n; i++) {
t1 = f(t1,t1);
t1 = f(t1, t1);
t2 = mk_let("x", expr(), t2, f(Var(0), Var(0)));
t3 = f(t3,t3);
t3 = f(t3, t3);
}
lean_assert(t1 != t2);
env.add_theorem("eqs1", Eq(t1,t2), Refl(Int, t1));
env.add_theorem("eqs2", Eq(t1,t3), Refl(Int, t1));
env.add_theorem("eqs1", Eq(t1, t2), Refl(Int, t1));
env.add_theorem("eqs2", Eq(t1, t3), Refl(Int, t1));
}
static expr mk_big(unsigned depth) {
@ -244,7 +244,7 @@ static void tst13() {
env.add_var("f", Type() >> Type());
expr f = Const("f");
std::cout << infer_type(f(Bool), env) << "\n";
std::cout << infer_type(f(Eq(True,False)), env) << "\n";
std::cout << infer_type(f(Eq(True, False)), env) << "\n";
}
int main() {

4
src/tests/library/light_checker.cpp
View file

@ -24,10 +24,10 @@ static void tst1() {
expr b = Const("b");
expr A = Const("A");
env.add_var("f", Int >> (Int >> Int));
lean_assert(type_of(f(a,a)) == Int);
lean_assert(type_of(f(a, a)) == Int);
lean_assert(type_of(f(a)) == Int >> Int);
lean_assert(type_of(And(a, f(a))) == Bool);
lean_assert(type_of(Fun({a, Int}, iAdd(a,iVal(1)))) == Int >> Int);
lean_assert(type_of(Fun({a, Int}, iAdd(a, iVal(1)))) == Int >> Int);
lean_assert(type_of(Let({a, iVal(10)}, iAdd(a, b))) == Int);
lean_assert(type_of(Type()) == Type(level() + 1));
lean_assert(type_of(Bool) == Type());

6
src/tests/library/metavar.cpp
View file

@ -51,7 +51,7 @@ static void tst3() {
expr r = instantiate_free_var_mmv(t, 0, a);
r = instantiate_metavar(r, 1, g(Var(0), Var(1)));
std::cout << r << std::endl;
lean_assert(r == f(g(a,Var(0)), a, Var(1)));
lean_assert(r == f(g(a, Var(0)), a, Var(1)));
}
static void tst4() {
@ -66,7 +66,7 @@ static void tst4() {
std::cout << r << std::endl;
r = instantiate_metavar(r, 1, g(Var(0), Var(1)));
std::cout << r << std::endl;
lean_assert(r == f(g(a,Var(2)), Var(2), Var(3)));
lean_assert(r == f(g(a, Var(2)), Var(2), Var(3)));
}
static void tst5() {
@ -98,7 +98,7 @@ static void tst6() {
expr a = Const("a");
expr x = Const("x");
expr m1 = mk_metavar(1);
expr t = mk_app(Fun({x,N}, m1), a);
expr t = mk_app(Fun({x, N}, m1), a);
expr s1 = instantiate_metavar(head_reduce_mmv(t, env), 1, Var(0));
expr s2 = head_reduce_mmv(instantiate_metavar(t, 1, Var(0)), env);
std::cout << instantiate_metavar(t, 1, Var(0)) << "\n";

2
src/tests/util/format.cpp
View file

@ -107,7 +107,7 @@ static void tst4() {
s << pp(sexpr()) << " ";
s << pp(sexpr("test")) << " ";
sexpr s1(mpz(100));
sexpr s2(mpq(1,2));
sexpr s2(mpq(1, 2));
sexpr s3{s1, s2};
s << pp(s3);
std::cout << s.str() << "\n";

4
src/tests/util/name.cpp
View file

@ -8,7 +8,7 @@ Author: Leonardo de Moura
#include <sstream>
#include "util/test.h"
#include "util/name.h"
using namespace lean;
using namespace lean;
static void tst1() {
name n("foo");
@ -27,7 +27,7 @@ static void tst1() {
lean_assert(name(name(), "foo") == name("foo"));
lean_assert(name(n, 1) < name(n, 2));
std::cout << "cmp(" << name(n, 1) << ", " << name(n, 2) << ") = " << cmp(name(n,1), name(n, 2)) << "\n";
std::cout << "cmp(" << name(n, 1) << ", " << name(n, 2) << ") = " << cmp(name(n, 1), name(n, 2)) << "\n";
lean_assert(!(name(n, 1) >= name(n, 2)));
lean_assert(name(n, 1) < name(name(n, 1), 1));
lean_assert(n < name(n, 1));

60
src/tests/util/numerics/mpbq.cpp
View file

@ -12,26 +12,26 @@ Author: Leonardo de Moura
using namespace lean;
static void tst1() {
mpbq a(1,1);
mpbq a(1, 1);
std::cout << a << "\n";
lean_assert(a == mpq(1,2));
std::cout << mpbq(mpq(1,3)) << "\n";
lean_assert(!set(a, mpq(1,3)));
lean_assert(a == mpbq(1,2));
lean_assert(a == mpq(1, 2));
std::cout << mpbq(mpq(1, 3)) << "\n";
lean_assert(!set(a, mpq(1, 3)));
lean_assert(a == mpbq(1, 2));
mpq b;
b = a;
lean_assert(b == mpq(1,4));
lean_assert(b == mpq(1, 4));
lean_assert(inv(b) == 4);
lean_assert(a/2 == mpbq(1,3));
lean_assert(a/2 == mpbq(1, 3));
lean_assert(a/1 == a);
lean_assert(a/8 == mpbq(1,5));
lean_assert((3*a)/8 == mpbq(3,5));
lean_assert(a/8 == mpbq(1, 5));
lean_assert((3*a)/8 == mpbq(3, 5));
mpbq l(0), u(1);
mpq v(1,3);
mpq v(1, 3);
while (true) {
lean_assert(l < v);
lean_assert(v < u);
std::cout << mpbq::decimal(l,20) << " " << v << " " << mpbq::decimal(u, 20) << "\n";
std::cout << mpbq::decimal(l, 20) << " " << v << " " << mpbq::decimal(u, 20) << "\n";
if (lt_1div2k((u - l)/2, 50))
break;
refine_lower(v, l, u);
@ -44,31 +44,31 @@ static void tst2() {
std::ostringstream out;
out << num;
lean_assert(out.str() == "2");
mpbq a(-1,2);
mpbq a(-1, 2);
std::ostringstream out2;
display_decimal(out2, a, 10);
lean_assert(out2.str() == "-0.25");
lean_assert(lt_1div2k(a, 8));
mul2(a);
lean_assert(a == mpbq(-1,1));
lean_assert(a == mpbq(-1, 1));
mul2k(a, 3);
lean_assert(a == mpbq(-4));
mul2k(a, 0);
lean_assert(a == mpbq(-4));
mul2k(a, 2);
lean_assert(a == mpbq(-16));
lean_assert(cmp(mpbq(1,2), mpbq(1,4)) == 1);
lean_assert(cmp(mpbq(1,2), mpbq(1,2)) == 0);
lean_assert(cmp(mpbq(1,2), mpbq(3,2)) == -1);
lean_assert(cmp(mpbq(3,2), mpbq(3,4)) == 1);
lean_assert(cmp(mpbq(15,2), mpbq(3,1)) == 1);
lean_assert(cmp(mpbq(7,1), mpz(3)) == 1);
lean_assert(cmp(mpbq(3,0), mpz(3)) == 0);
lean_assert(cmp(mpbq(2,0), mpz(3)) == -1);
lean_assert(cmp(mpbq(7,4), mpz(10)) == -1);
lean_assert(mpbq(0,1) == mpz(0));
set(a, mpq(1,4));
lean_assert(cmp(a, mpbq(1,2)) == 0);
lean_assert(cmp(mpbq(1, 2), mpbq(1, 4)) == 1);
lean_assert(cmp(mpbq(1, 2), mpbq(1, 2)) == 0);
lean_assert(cmp(mpbq(1, 2), mpbq(3, 2)) == -1);
lean_assert(cmp(mpbq(3, 2), mpbq(3, 4)) == 1);
lean_assert(cmp(mpbq(15, 2), mpbq(3, 1)) == 1);
lean_assert(cmp(mpbq(7, 1), mpz(3)) == 1);
lean_assert(cmp(mpbq(3, 0), mpz(3)) == 0);
lean_assert(cmp(mpbq(2, 0), mpz(3)) == -1);
lean_assert(cmp(mpbq(7, 4), mpz(10)) == -1);
lean_assert(mpbq(0, 1) == mpz(0));
set(a, mpq(1, 4));
lean_assert(cmp(a, mpbq(1, 2)) == 0);
set(a, mpq(0));
lean_assert(a.is_zero());
a += 3u;
@ -76,15 +76,15 @@ static void tst2() {
a += -2;
lean_assert(a == 1);
div2k(a, 2);
lean_assert(a == mpq(1,4));
lean_assert(a == mpq(1, 4));
a += 3u;
lean_assert(a == mpq(13,4));
lean_assert(a == mpq(13, 4));
a += -2;
lean_assert(a == mpq(5,4));
lean_assert(a == mpq(5, 4));
a -= 1u;
lean_assert(a == mpq(1,4));
lean_assert(a == mpq(1, 4));
a -= -2;
lean_assert(a == mpq(9,4));
lean_assert(a == mpq(9, 4));
}
int main() {

70
src/tests/util/numerics/mpq.cpp
View file

@ -17,9 +17,9 @@ static void tst0() {
}
static void tst1() {
mpq a(2,3), b(4,3);
mpq a(2, 3), b(4, 3);
b = a / b;
lean_assert(b == mpq(1,2));
lean_assert(b == mpq(1, 2));
a = mpq(2);
a.inv();
lean_assert(a == b);
@ -30,7 +30,7 @@ static void tst1() {
}
static void tst2() {
mpq a(2,3);
mpq a(2, 3);
lean_assert(floor(a) == 0);
lean_assert(ceil(a) == 1);
mpq b(-2, 3);
@ -58,35 +58,35 @@ static void tst3() {
}
static void tst4() {
mpq a(8,6);
lean_assert(a == mpq(4,3));
lean_assert(mpq(1,2)+mpq(1,2) == mpq(1));
mpq a(8, 6);
lean_assert(a == mpq(4, 3));
lean_assert(mpq(1, 2)+mpq(1, 2) == mpq(1));
lean_assert(mpq("1/2") < mpq("2/3"));
lean_assert(mpq(-1,2).is_neg());
lean_assert(mpq(-1,2).is_nonpos());
lean_assert(!mpq(-1,2).is_zero());
lean_assert(mpq(1,2) > mpq());
lean_assert(mpq(-1, 2).is_neg());
lean_assert(mpq(-1, 2).is_nonpos());
lean_assert(!mpq(-1, 2).is_zero());
lean_assert(mpq(1, 2) > mpq());
lean_assert(mpq().is_zero());
lean_assert(mpq(2,3) + mpq(4,3) == mpq(2));
lean_assert(mpq(1,2) >= mpq(1,3));
lean_assert(mpq(3,4).get_denominator() == 4);
lean_assert(mpq(3,4).get_numerator() == 3);
lean_assert(mpq(1,2) / mpq(5,4) == mpq(2,5));
lean_assert(mpq(1,2) - mpq(2,3) == mpq(-1,6));
lean_assert(mpq(3,4) * mpq(2,3) == mpq(1,2));
lean_assert(mpq(2, 3) + mpq(4, 3) == mpq(2));
lean_assert(mpq(1, 2) >= mpq(1, 3));
lean_assert(mpq(3, 4).get_denominator() == 4);
lean_assert(mpq(3, 4).get_numerator() == 3);
lean_assert(mpq(1, 2) / mpq(5, 4) == mpq(2, 5));
lean_assert(mpq(1, 2) - mpq(2, 3) == mpq(-1, 6));
lean_assert(mpq(3, 4) * mpq(2, 3) == mpq(1, 2));
a *= 3;
lean_assert(a == 4);
a /= 2;
lean_assert(a == 2);
lean_assert(a.is_integer());
a /= 5;
lean_assert(a == mpq(2,5));
lean_assert(a == mpq(2, 5));
lean_assert(!a.is_integer());
mpq b(3,7);
mpq b(3, 7);
a *= b;
lean_assert(a == mpq(6,35));
lean_assert(a == mpq(6, 35));
a /= b;
lean_assert(a == mpq(2,5));
lean_assert(a == mpq(2, 5));
mpz c(5);
a *= c;
lean_assert(a == 2);
@ -95,7 +95,7 @@ static void tst4() {
a -= c;
lean_assert(a == 2);
a /= c;
lean_assert(a == mpq(2,5));
lean_assert(a == mpq(2, 5));
}
static void tst5() {
@ -123,7 +123,7 @@ static void tst5() {
lean_assert(1u >= a);
lean_assert(2u > a);
a = "1/3";
lean_assert(a == mpq(1,3));
lean_assert(a == mpq(1, 3));
a = 2.0;
lean_assert(a == mpq(2));
a = mpz(10);
@ -147,30 +147,30 @@ static void tst6() {
lean_assert(v1 == 1);
v1.ceil();
lean_assert(v1 == 1);
v1 = mpq(1,2);
v1 = mpq(1, 2);
v1.floor();
lean_assert(v1 == 0);
v1 = mpq(1,2);
v1 = mpq(1, 2);
v1.ceil();
lean_assert(v1 == 1);
v1 -= 2u;
lean_assert(v1 == -1);
v1 = mpq(-1,2);
v1 = mpq(-1, 2);
v1.floor();
lean_assert(v1 == -1);
v1 = mpq(-1,2);
v1 = mpq(-1, 2);
v1.ceil();
lean_assert(v1 == 0);
check_dec(mpq(-1,2), "-0.5");
check_dec(mpq(1,3), "0.33333?", 5);
check_dec(mpq(-1, 2), "-0.5");
check_dec(mpq(1, 3), "0.33333?", 5);
check_dec(mpq(3), "3");
check_dec(mpq(-2,1), "-2");
check_dec(mpq(-1,3), "-0.33333?", 5);
check_dec(mpq(-1,7), "-0.14285?", 5);
check_dec(mpq(-2, 1), "-2");
check_dec(mpq(-1, 3), "-0.33333?", 5);
check_dec(mpq(-1, 7), "-0.14285?", 5);
lean_assert(cmp(mpq(1,2), mpz(1)) < 0);
lean_assert(cmp(mpq(3,2), mpz(1)) > 0);
lean_assert(cmp(mpq(-3,2), mpz(-1)) < 0);
lean_assert(cmp(mpq(1, 2), mpz(1)) < 0);
lean_assert(cmp(mpq(3, 2), mpz(1)) > 0);
lean_assert(cmp(mpq(-3, 2), mpz(-1)) < 0);
}
int main() {

32
src/tests/util/sexpr.cpp
View file

@ -49,9 +49,9 @@ static void tst1() {
lean_assert(is_list(sexpr{10.2}));
lean_assert(len(sexpr{10.2}) == 1);
// list of pairs
std::cout << sexpr{ sexpr(1,2), sexpr(2,3), sexpr(0,1) } << "\n";
std::cout << sexpr{ sexpr(1, 2), sexpr(2, 3), sexpr(0, 1) } << "\n";
// list of lists
std::cout << sexpr{ sexpr{1,2}, sexpr{2,3}, sexpr{0,1} } << "\n";
std::cout << sexpr{ sexpr{1, 2}, sexpr{2, 3}, sexpr{0, 1} } << "\n";
lean_assert(reverse(sexpr{1, 2, 3}) == (sexpr{3, 2, 1}));
sexpr l = map(sexpr{1, 2, 3},
[](sexpr e) {
@ -67,11 +67,11 @@ static void tst1() {
lean_assert(member(3, sexpr{10, 2, 3, 1}));
lean_assert(!member(3, nil()));
lean_assert(!member(3, sexpr{10, 2, 1}));
lean_assert(append(sexpr{1,2}, sexpr{3,4}) == (sexpr{1,2,3,4}));
lean_assert(append(sexpr{1, 2}, sexpr{3, 4}) == (sexpr{1, 2, 3, 4}));
lean_assert(append(l, nil()) == l);
lean_assert(append(nil(), l) == l);
lean_assert(contains(sexpr{10,20,-2,0,10}, [](sexpr e) { return to_int(e) < 0; }));
lean_assert(!contains(sexpr{10,20,-2,0,10}, [](sexpr e) { return to_int(e) < -10; }));
lean_assert(contains(sexpr{10, 20, -2, 0, 10}, [](sexpr e) { return to_int(e) < 0; }));
lean_assert(!contains(sexpr{10, 20, -2, 0, 10}, [](sexpr e) { return to_int(e) < -10; }));
lean_assert(is_eqp(s1, s1));
sexpr s3 = s1;
lean_assert(is_eqp(s1, s3));
@ -101,12 +101,12 @@ static void tst2() {
lean_assert(a == sexpr(name(name("foo"), 1)));
lean_assert(a == name(name("foo"), 1));
lean_assert(name(name("foo"), 1) == a);
a = mpq(1,3);
lean_assert(a == sexpr(mpq(1,3)));
lean_assert(a == mpq(1,3));
a = mpq(1, 3);
lean_assert(a == sexpr(mpq(1, 3)));
lean_assert(a == mpq(1, 3));
lean_assert(mpq(1, 3) == a);
lean_assert(mpq(2, 3) != a);
a = power(mpz(2),100);
a = power(mpz(2), 100);
lean_assert(a == sexpr(power(mpz(2), 100)));
lean_assert(a == power(mpz(2), 100));
lean_assert(power(mpz(2), 100) == a);
@ -142,14 +142,14 @@ static void tst4() {
}
static void tst5() {
lean_assert(foldl(sexpr{1,2,3,4,5,6,7,8,9},
lean_assert(foldl(sexpr{1, 2, 3, 4, 5, 6, 7, 8, 9},
0,
[](int result, sexpr const & s) {
return result * 10 + to_int(s);
})
== 123456789);
lean_assert(foldr(sexpr{1,2,3,4,5,6,7,8,9},
lean_assert(foldr(sexpr{1, 2, 3, 4, 5, 6, 7, 8, 9},
0,
[](sexpr const & s, int result) {
return result * 10 + to_int(s);
@ -165,9 +165,9 @@ static void tst6() {
}
static void tst7() {
sexpr s = sexpr{ sexpr(1,2), sexpr(2,3), sexpr(0,1) };
sexpr s = sexpr{ sexpr(1, 2), sexpr(2, 3), sexpr(0, 1) };
std::cout << pp(sexpr{s, s, s, s, s}) << "\n";
std::cout << pp(sexpr{sexpr(name{"test","name"}), sexpr(10), sexpr(10.20)}) << "\n";
std::cout << pp(sexpr{sexpr(name{"test", "name"}), sexpr(10), sexpr(10.20)}) << "\n";
format f = highlight(pp(sexpr{s, s, s, s, s}));
std::cout << f << "\n";
std::cout << mk_pair(f, options({"pp", "width"}, 1000)) << "\n";
@ -194,10 +194,10 @@ static void tst8() {
lean_assert(cmp(sexpr(name("aaa")), sexpr(name("bbb"))) < 0);
lean_assert(cmp(sexpr(mpz(10)), sexpr(mpz(10))) == 0);
lean_assert(cmp(sexpr(mpz(20)), sexpr(mpz(10))) > 0);
lean_assert(cmp(sexpr(mpq(1,2)), sexpr(mpq(1,2))) == 0);
lean_assert(cmp(sexpr(mpq(1,3)), sexpr(mpq(1,2))) < 0);
lean_assert(cmp(sexpr(mpq(1, 2)), sexpr(mpq(1, 2))) == 0);
lean_assert(cmp(sexpr(mpq(1, 3)), sexpr(mpq(1, 2))) < 0);
std::ostringstream s;
s << sexpr() << " " << sexpr(mpq(1,2));
s << sexpr() << " " << sexpr(mpq(1, 2));
std::cout << s.str() << "\n";
lean_assert(s.str() == "nil 1/2");
}

4
src/util/hash.cpp
View file

@ -33,7 +33,7 @@ unsigned hash_str(unsigned length, char const * str, unsigned init_value) {
a += reinterpret_cast<unsigned const *>(str)[0];
b += reinterpret_cast<unsigned const *>(str)[1];
c += reinterpret_cast<unsigned const *>(str)[2];
mix(a,b,c);
mix(a, b, c);
str += 12; len -= 12;
}
@ -55,7 +55,7 @@ unsigned hash_str(unsigned length, char const * str, unsigned init_value) {
case 1 : a+=str[0];
/* case 0: nothing left to add */
}
mix(a,b,c);
mix(a, b, c);
/*-------------------------------------------- report the result */
return c;
}

18
src/util/numerics/mpbq.h
View file

@ -124,15 +124,15 @@ public:
friend bool operator==(unsigned int a, mpbq const & b) { return operator==(b, a); }
friend bool operator==(int a, mpbq const & b) { return operator==(b, a); }
friend bool operator!=(mpbq const & a, mpbq const & b) { return !operator==(a,b); }
friend bool operator!=(mpbq const & a, mpz const & b) { return !operator==(a,b); }
friend bool operator!=(mpbq const & a, mpq const & b) { return !operator==(a,b); }
friend bool operator!=(mpbq const & a, unsigned int b) { return !operator==(a,b); }
friend bool operator!=(mpbq const & a, int b) { return !operator==(a,b); }
friend bool operator!=(mpz const & a, mpbq const & b) { return !operator==(a,b); }
friend bool operator!=(mpq const & a, mpbq const & b) { return !operator==(a,b); }
friend bool operator!=(unsigned int a, mpbq const & b) { return !operator==(a,b); }
friend bool operator!=(int a, mpbq const & b) { return !operator==(a,b); }
friend bool operator!=(mpbq const & a, mpbq const & b) { return !operator==(a, b); }
friend bool operator!=(mpbq const & a, mpz const & b) { return !operator==(a, b); }
friend bool operator!=(mpbq const & a, mpq const & b) { return !operator==(a, b); }
friend bool operator!=(mpbq const & a, unsigned int b) { return !operator==(a, b); }
friend bool operator!=(mpbq const & a, int b) { return !operator==(a, b); }
friend bool operator!=(mpz const & a, mpbq const & b) { return !operator==(a, b); }
friend bool operator!=(mpq const & a, mpbq const & b) { return !operator==(a, b); }
friend bool operator!=(unsigned int a, mpbq const & b) { return !operator==(a, b); }
friend bool operator!=(int a, mpbq const & b) { return !operator==(a, b); }
mpbq & operator+=(mpbq const & a);
mpbq & operator+=(unsigned a);

2
src/util/numerics/mpfp.h
View file

@ -299,7 +299,7 @@ public:
friend bool operator==(mpfp const & a, mpq_t const & b ) { return cmp(a, b) == 0; }
friend bool operator==(mpfp const & a, mpf_t const & b ) { return cmp(a, b) == 0; }
friend bool operator!=(mpfp const & a, mpfp const & b) { return !operator==(a,b); }
friend bool operator!=(mpfp const & a, mpfp const & b) { return !operator==(a, b); }
friend bool operator!=(unsigned long int const a, mpfp const & b) { return cmp(b, a) != 0; }
friend bool operator!=(long int const a , mpfp const & b) { return cmp(b, a) != 0; }
friend bool operator!=(double const a , mpfp const & b) { return cmp(b, a) != 0; }

14
src/util/numerics/mpq.h
View file

@ -121,13 +121,13 @@ public:
friend bool operator==(unsigned int a, mpq const & b) { return operator==(b, a); }
friend bool operator==(int a, mpq const & b) { return operator==(b, a); }
friend bool operator!=(mpq const & a, mpq const & b) { return !operator==(a,b); }
friend bool operator!=(mpq const & a, mpz const & b) { return !operator==(a,b); }
friend bool operator!=(mpq const & a, unsigned int b) { return !operator==(a,b); }
friend bool operator!=(mpq const & a, int b) { return !operator==(a,b); }
friend bool operator!=(mpz const & a, mpq const & b) { return !operator==(a,b); }
friend bool operator!=(unsigned int a, mpq const & b) { return !operator==(a,b); }
friend bool operator!=(int a, mpq const & b) { return !operator==(a,b); }
friend bool operator!=(mpq const & a, mpq const & b) { return !operator==(a, b); }
friend bool operator!=(mpq const & a, mpz const & b) { return !operator==(a, b); }
friend bool operator!=(mpq const & a, unsigned int b) { return !operator==(a, b); }
friend bool operator!=(mpq const & a, int b) { return !operator==(a, b); }
friend bool operator!=(mpz const & a, mpq const & b) { return !operator==(a, b); }
friend bool operator!=(unsigned int a, mpq const & b) { return !operator==(a, b); }
friend bool operator!=(int a, mpq const & b) { return !operator==(a, b); }
mpq & operator+=(mpq const & o) { mpq_add(m_val, m_val, o.m_val); return *this; }
mpq & operator+=(mpz const & o) { mpz_addmul(mpq_numref(m_val), mpq_denref(m_val), o.m_val); mpq_canonicalize(m_val); return *this; }

2
src/util/numerics/xnumeral.h
View file

@ -186,7 +186,7 @@ void power(T & a, xnumeral_kind & ak, unsigned n) {
}
/**
\brief Return true if (a,ak) == (b,bk).
\brief Return true if (a, ak) == (b, bk).
*/
template<typename T>
bool eq(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) {

8
src/util/sexpr/options.h
View file

@ -70,8 +70,8 @@ struct mk_option_declaration {
#define LEAN_MAKE_OPTION_NAME_CORE(LINE) LEAN_OPTION_ ## LINE
#define LEAN_MAKE_OPTION_NAME(LINE) LEAN_MAKE_OPTION_NAME_CORE(LINE)
#define LEAN_OPTION_UNIQUE_NAME LEAN_MAKE_OPTION_NAME(__LINE__)
#define RegisterOption(N,K,D,DESC) static ::lean::mk_option_declaration LEAN_OPTION_UNIQUE_NAME(N,K,D,DESC)
#define RegisterOptionCore(N,K,D,DESC) RegisterOption(N,K,#D,DESC)
#define RegisterBoolOption(N,D,DESC) RegisterOptionCore(N, BoolOption, D, DESC);
#define RegisterUnsignedOption(N,D,DESC) RegisterOptionCore(N, UnsignedOption, D, DESC);
#define RegisterOption(N, K, D, DESC) static ::lean::mk_option_declaration LEAN_OPTION_UNIQUE_NAME(N, K, D, DESC)
#define RegisterOptionCore(N, K, D, DESC) RegisterOption(N, K, #D, DESC)
#define RegisterBoolOption(N, D, DESC) RegisterOptionCore(N, BoolOption, D, DESC);
#define RegisterUnsignedOption(N, D, DESC) RegisterOptionCore(N, UnsignedOption, D, DESC);
}