diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 281d6dd55..1cd2db739 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -48,7 +48,7 @@ expr app(unsigned n, expr const * as) { unsigned new_n; unsigned n0 = 0; expr const & arg0 = as[0]; - // Remark: we represet ((app a b) c) as (app a b c) + // Remark: we represent ((app a b) c) as (app a b c) if (is_app(arg0)) { n0 = num_args(arg0); new_n = n + n0 - 1; diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 834a36fe4..7f55c776c 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -28,6 +28,8 @@ void tst1() { std::cout << lambda("x", prop(), var(0)) << "\n"; lean_assert(f(a)(a) == f(a, a)); lean_assert(f(a(a)) != f(a, a)); + lean_assert(lambda("x", prop(), var(0)) == lambda("y", prop(), var(0))); + std::cout << pi("x", prop(), var(0)) << "\n"; } expr mk_dag(unsigned depth, bool _closed = false) { @@ -245,6 +247,15 @@ void tst10() { } } +void tst11() { + expr f = constant("f"); + expr a = constant("a"); + expr y = var(0); + expr x = var(0); + lean_assert(closed(lambda("bla", prop(), lambda("x", prop(), f(f(a, a, x), y))))); +} + + int main() { continue_on_violation(true); std::cout << "sizeof(expr): " << sizeof(expr) << "\n"; @@ -259,6 +270,7 @@ int main() { tst8(); tst9(); tst10(); + tst11(); std::cout << "done" << "\n"; return has_violations() ? 1 : 0; } diff --git a/src/tests/sexpr/sexpr.cpp b/src/tests/sexpr/sexpr.cpp index b6a15bfa6..531bdaf01 100644 --- a/src/tests/sexpr/sexpr.cpp +++ b/src/tests/sexpr/sexpr.cpp @@ -73,6 +73,7 @@ static void tst1() { sexpr s3 = s1; lean_assert(eqp(s1, s3)); lean_assert(!eqp(sexpr(1), sexpr(1))); + lean_assert(is_list(nil())); } static void tst2() {