From 9c60eed93c24f97c882504393d16417b1fbb3203 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 Nov 2013 10:16:22 -0800 Subject: [PATCH] refactor(kernel/metavar): avoid using unique names for default metavariable prefix The problem is that unique names depend on the order compilation units are initialized. The order of initialization is not specified by the C++ standard. Then, different compilers (or even the same compiler) may produce different initialization orders, and consequently the metavariable prefix is going to be different for different builds. This is not a bug, but it makes unit tests to fail since the output produced by different builds is different for the same input file. Avoiding unique name feature in the default metavariable prefix avoids this problem. Signed-off-by: Leonardo de Moura --- src/frontends/lean/pp.cpp | 2 +- src/kernel/metavar.cpp | 5 +- src/kernel/printer.cpp | 2 +- src/tests/kernel/metavar.cpp | 2 +- tests/lean/elab1.lean.expected.out | 457 ++++++++++++------------- tests/lean/ex3.lean.expected.out | 16 +- tests/lean/let4.lean.expected.out | 30 +- tests/lean/overload2.lean.expected.out | 92 ++--- tests/lean/tst7.lean.expected.out | 2 +- tests/lean/tst9.lean.expected.out | 4 +- 10 files changed, 298 insertions(+), 314 deletions(-) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 4ec4f0c78..2c528bb0e 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1043,7 +1043,7 @@ class pp_fn { } result pp_metavar(expr const & a, unsigned depth) { - format mv_fmt = compose(format("?M"), format(metavar_name(a))); + format mv_fmt = compose(format("?"), format(metavar_name(a))); if (metavar_lctx(a)) { format ctx_fmt; bool first = true; diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 8a3ade612..433e0f2b1 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -50,8 +50,6 @@ public: virtual expr const & get_main_expr() const { return m_expr; } }; -static name g_unique_name = name::mk_internal_unique_name(); - void swap(metavar_env & a, metavar_env & b) { swap(a.m_name_generator, b.m_name_generator); swap(a.m_metavar_data, b.m_metavar_data); @@ -75,8 +73,9 @@ metavar_env::metavar_env(name const & prefix): m_timestamp(0) { } +static name g_default_name("M"); metavar_env::metavar_env(): - metavar_env(g_unique_name) { + metavar_env(g_default_name) { } expr metavar_env::mk_metavar(context const & ctx, expr const & type) { diff --git a/src/kernel/printer.cpp b/src/kernel/printer.cpp index e07f6c80f..87681109e 100644 --- a/src/kernel/printer.cpp +++ b/src/kernel/printer.cpp @@ -76,7 +76,7 @@ struct print_expr_fn { } void print_metavar(expr const & a, context const &) { - out() << "?M" << metavar_name(a); + out() << "?" << metavar_name(a); if (metavar_lctx(a)) { out() << "["; bool first = true; diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index 2b2554dfd..d4d7c7537 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -28,7 +28,7 @@ static std::ostream & operator<<(std::ostream & out, metavar_env const & menv) { bool first = true; menv.for_each_subst([&](name const & n, expr const & v) { if (first) first = false; else out << "\n"; - out << "?M" << n << " <- " << v; + out << "?" << n << " <- " << v; }); return out; } diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out index 7fb9cea85..4834367dc 100644 --- a/tests/lean/elab1.lean.expected.out +++ b/tests/lean/elab1.lean.expected.out @@ -2,122 +2,122 @@ Set: pp::unicode Assumed: f Failed to solve - ⊢ (?M3::1 ≈ λ x : ℕ, x) ⊕ (?M3::1 ≈ nat_to_int) ⊕ (?M3::1 ≈ nat_to_real) + ⊢ (?M::1 ≈ λ x : ℕ, x) ⊕ (?M::1 ≈ nat_to_int) ⊕ (?M::1 ≈ nat_to_real) (line: 4: pos: 8) Coercion for 10 Failed to solve ⊢ Bool ≺ ℕ Substitution - ⊢ Bool ≺ ?M3::0 + ⊢ Bool ≺ ?M::0 (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 - ?M3::1 10 + ?M::0 + ?M::1 10 ⊤ Assignment - ⊢ ℕ ≺ ?M3::0 + ⊢ ℕ ≺ ?M::0 Substitution - ⊢ (?M3::5[inst:0 (10)]) 10 ≺ ?M3::0 + ⊢ (?M::5[inst:0 (10)]) 10 ≺ ?M::0 (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 - ?M3::1 10 + ?M::0 + ?M::1 10 ⊤ Assignment - x : ℕ ⊢ λ x : ℕ, ℕ ≈ ?M3::5 + x : ℕ ⊢ λ x : ℕ, ℕ ≈ ?M::5 Destruct/Decompose - x : ℕ ⊢ ℕ ≈ ?M3::5 x + x : ℕ ⊢ ℕ ≈ ?M::5 x Destruct/Decompose - ⊢ ℕ → ℕ ≈ Π x : ?M3::4, ?M3::5 x + ⊢ ℕ → ℕ ≈ Π x : ?M::4, ?M::5 x Substitution - ⊢ ?M3::3 ≈ Π x : ?M3::4, ?M3::5 x + ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x Function expected at - ?M3::1 10 + ?M::1 10 Assignment - ⊢ ℕ → ℕ ≺ ?M3::3 - Propagate type, ?M3::1 : ?M3::3 + ⊢ ℕ → ℕ ≺ ?M::3 + Propagate type, ?M::1 : ?M::3 Assignment - ⊢ ?M3::1 ≈ λ x : ℕ, x + ⊢ ?M::1 ≈ λ x : ℕ, x Assumption 0 Failed to solve ⊢ Bool ≺ ℤ Substitution - ⊢ Bool ≺ ?M3::0 + ⊢ Bool ≺ ?M::0 (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 - ?M3::1 10 + ?M::0 + ?M::1 10 ⊤ Assignment - ⊢ ℤ ≺ ?M3::0 + ⊢ ℤ ≺ ?M::0 Substitution - ⊢ (?M3::5[inst:0 (10)]) 10 ≺ ?M3::0 + ⊢ (?M::5[inst:0 (10)]) 10 ≺ ?M::0 (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 - ?M3::1 10 + ?M::0 + ?M::1 10 ⊤ Assignment - _ : ℕ ⊢ λ x : ℕ, ℤ ≈ ?M3::5 + _ : ℕ ⊢ λ x : ℕ, ℤ ≈ ?M::5 Destruct/Decompose - _ : ℕ ⊢ ℤ ≈ ?M3::5 _ + _ : ℕ ⊢ ℤ ≈ ?M::5 _ Destruct/Decompose - ⊢ ℕ → ℤ ≈ Π x : ?M3::4, ?M3::5 x + ⊢ ℕ → ℤ ≈ Π x : ?M::4, ?M::5 x Substitution - ⊢ ?M3::3 ≈ Π x : ?M3::4, ?M3::5 x + ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x Function expected at - ?M3::1 10 + ?M::1 10 Assignment - ⊢ ℕ → ℤ ≺ ?M3::3 - Propagate type, ?M3::1 : ?M3::3 + ⊢ ℕ → ℤ ≺ ?M::3 + Propagate type, ?M::1 : ?M::3 Assignment - ⊢ ?M3::1 ≈ nat_to_int + ⊢ ?M::1 ≈ nat_to_int Assumption 1 Failed to solve ⊢ Bool ≺ ℝ Substitution - ⊢ Bool ≺ ?M3::0 + ⊢ Bool ≺ ?M::0 (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 - ?M3::1 10 + ?M::0 + ?M::1 10 ⊤ Assignment - ⊢ ℝ ≺ ?M3::0 + ⊢ ℝ ≺ ?M::0 Substitution - ⊢ (?M3::5[inst:0 (10)]) 10 ≺ ?M3::0 + ⊢ (?M::5[inst:0 (10)]) 10 ≺ ?M::0 (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 - ?M3::1 10 + ?M::0 + ?M::1 10 ⊤ Assignment - _ : ℕ ⊢ λ x : ℕ, ℝ ≈ ?M3::5 + _ : ℕ ⊢ λ x : ℕ, ℝ ≈ ?M::5 Destruct/Decompose - _ : ℕ ⊢ ℝ ≈ ?M3::5 _ + _ : ℕ ⊢ ℝ ≈ ?M::5 _ Destruct/Decompose - ⊢ ℕ → ℝ ≈ Π x : ?M3::4, ?M3::5 x + ⊢ ℕ → ℝ ≈ Π x : ?M::4, ?M::5 x Substitution - ⊢ ?M3::3 ≈ Π x : ?M3::4, ?M3::5 x + ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x Function expected at - ?M3::1 10 + ?M::1 10 Assignment - ⊢ ℕ → ℝ ≺ ?M3::3 - Propagate type, ?M3::1 : ?M3::3 + ⊢ ℕ → ℝ ≺ ?M::3 + Propagate type, ?M::1 : ?M::3 Assignment - ⊢ ?M3::1 ≈ nat_to_real + ⊢ ?M::1 ≈ nat_to_real Assumption 2 Assumed: g Error (line: 7, pos: 8) unexpected metavariable occurrence Assumed: h Failed to solve -x : ?M3::0, A : Type ⊢ ?M3::0[lift:0:2] ≺ A +x : ?M::0, A : Type ⊢ ?M::0[lift:0:2] ≺ A (line: 11: pos: 27) Type of argument 2 must be convertible to the expected type in the application of h with arguments: @@ -125,7 +125,7 @@ x : ?M3::0, A : Type ⊢ ?M3::0[lift:0:2] ≺ A x Assumed: my_eq Failed to solve -A : Type, B : Type, a : ?M3::0, b : ?M3::1, C : Type ⊢ ?M3::0[lift:0:3] ≺ C +A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C (line: 15: pos: 51) Type of argument 2 must be convertible to the expected type in the application of my_eq with arguments: @@ -139,557 +139,542 @@ Error (line: 20, pos: 28) unexpected metavariable occurrence Failed to solve ⊢ b ≈ a Substitution - ⊢ b ≈ ?M3::3 + ⊢ b ≈ ?M::3 Destruct/Decompose - ⊢ b == b ≺ ?M3::3 == ?M3::4 + ⊢ b == b ≺ ?M::3 == ?M::4 (line: 22: pos: 22) Type of argument 6 must be convertible to the expected type in the application of Trans::explicit with arguments: - ?M3::1 - ?M3::2 - ?M3::3 - ?M3::4 + ?M::1 + ?M::2 + ?M::3 + ?M::4 Refl a Refl b Assignment - ⊢ a ≈ ?M3::3 + ⊢ a ≈ ?M::3 Destruct/Decompose - ⊢ a == a ≺ ?M3::2 == ?M3::3 + ⊢ a == a ≺ ?M::2 == ?M::3 (line: 22: pos: 22) Type of argument 5 must be convertible to the expected type in the application of Trans::explicit with arguments: - ?M3::1 - ?M3::2 - ?M3::3 - ?M3::4 + ?M::1 + ?M::2 + ?M::3 + ?M::4 Refl a Refl b Failed to solve - ⊢ (?M3::0 ≈ Type) ⊕ (?M3::0 ≈ Type 1) ⊕ (?M3::0 ≈ Type 2) ⊕ (?M3::0 ≈ Type M) ⊕ (?M3::0 ≈ Type U) + ⊢ (?M::0 ≈ Type) ⊕ (?M::0 ≈ Type 1) ⊕ (?M::0 ≈ Type 2) ⊕ (?M::0 ≈ Type M) ⊕ (?M::0 ≈ Type U) Destruct/Decompose - ⊢ Type ≺ ?M3::0 + ⊢ Type ≺ ?M::0 (line: 24: pos: 6) Type of argument 3 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Failed to solve - ⊢ - (?M3::1 ≈ Type 1) ⊕ (?M3::1 ≈ Type 2) ⊕ (?M3::1 ≈ Type 3) ⊕ (?M3::1 ≈ Type M) ⊕ (?M3::1 ≈ Type U) + ⊢ (?M::1 ≈ Type 1) ⊕ (?M::1 ≈ Type 2) ⊕ (?M::1 ≈ Type 3) ⊕ (?M::1 ≈ Type M) ⊕ (?M::1 ≈ Type U) Destruct/Decompose - ⊢ Type 1 ≺ ?M3::1 - Propagate type, ?M3::0 : ?M3::1 + ⊢ Type 1 ≺ ?M::1 + Propagate type, ?M::0 : ?M::1 Assignment - ⊢ ?M3::0 ≈ Type + ⊢ ?M::0 ≈ Type Assumption 0 Failed to solve ⊢ Type 1 ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type 1 + ⊢ ?M::1 ≈ Type 1 Assumption 1 Failed to solve ⊢ Type 2 ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type 2 + ⊢ ?M::1 ≈ Type 2 Assumption 2 Failed to solve ⊢ Type 3 ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type 3 + ⊢ ?M::1 ≈ Type 3 Assumption 3 Failed to solve ⊢ Type M ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type M + ⊢ ?M::1 ≈ Type M Assumption 4 Failed to solve ⊢ Type U ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type U + ⊢ ?M::1 ≈ Type U Assumption 5 Failed to solve - ⊢ - (?M3::1 ≈ Type 2) ⊕ (?M3::1 ≈ Type 3) ⊕ (?M3::1 ≈ Type 4) ⊕ (?M3::1 ≈ Type M) ⊕ (?M3::1 ≈ Type U) + ⊢ (?M::1 ≈ Type 2) ⊕ (?M::1 ≈ Type 3) ⊕ (?M::1 ≈ Type 4) ⊕ (?M::1 ≈ Type M) ⊕ (?M::1 ≈ Type U) Destruct/Decompose - ⊢ Type 2 ≺ ?M3::1 - Propagate type, ?M3::0 : ?M3::1 + ⊢ Type 2 ≺ ?M::1 + Propagate type, ?M::0 : ?M::1 Assignment - ⊢ ?M3::0 ≈ Type 1 + ⊢ ?M::0 ≈ Type 1 Assumption 6 Failed to solve ⊢ Type 2 ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type 2 + ⊢ ?M::1 ≈ Type 2 Assumption 7 Failed to solve ⊢ Type 3 ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type 3 + ⊢ ?M::1 ≈ Type 3 Assumption 8 Failed to solve ⊢ Type 4 ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type 4 + ⊢ ?M::1 ≈ Type 4 Assumption 9 Failed to solve ⊢ Type M ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type M + ⊢ ?M::1 ≈ Type M Assumption 10 Failed to solve ⊢ Type U ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type U + ⊢ ?M::1 ≈ Type U Assumption 11 Failed to solve - ⊢ - (?M3::1 ≈ Type 3) ⊕ (?M3::1 ≈ Type 4) ⊕ (?M3::1 ≈ Type 5) ⊕ (?M3::1 ≈ Type M) ⊕ (?M3::1 ≈ Type U) + ⊢ (?M::1 ≈ Type 3) ⊕ (?M::1 ≈ Type 4) ⊕ (?M::1 ≈ Type 5) ⊕ (?M::1 ≈ Type M) ⊕ (?M::1 ≈ Type U) Destruct/Decompose - ⊢ Type 3 ≺ ?M3::1 - Propagate type, ?M3::0 : ?M3::1 + ⊢ Type 3 ≺ ?M::1 + Propagate type, ?M::0 : ?M::1 Assignment - ⊢ ?M3::0 ≈ Type 2 + ⊢ ?M::0 ≈ Type 2 Assumption 12 Failed to solve ⊢ Type 3 ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type 3 + ⊢ ?M::1 ≈ Type 3 Assumption 13 Failed to solve ⊢ Type 4 ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type 4 + ⊢ ?M::1 ≈ Type 4 Assumption 14 Failed to solve ⊢ Type 5 ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type 5 + ⊢ ?M::1 ≈ Type 5 Assumption 15 Failed to solve ⊢ Type M ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type M + ⊢ ?M::1 ≈ Type M Assumption 16 Failed to solve ⊢ Type U ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type U + ⊢ ?M::1 ≈ Type U Assumption 17 Failed to solve ⊢ - (?M3::1 ≈ Type M+1) ⊕ - (?M3::1 ≈ Type M+2) ⊕ - (?M3::1 ≈ Type M+3) ⊕ - (?M3::1 ≈ Type M) ⊕ - (?M3::1 ≈ Type U) + (?M::1 ≈ Type M+1) ⊕ (?M::1 ≈ Type M+2) ⊕ (?M::1 ≈ Type M+3) ⊕ (?M::1 ≈ Type M) ⊕ (?M::1 ≈ Type U) Destruct/Decompose - ⊢ Type M+1 ≺ ?M3::1 - Propagate type, ?M3::0 : ?M3::1 + ⊢ Type M+1 ≺ ?M::1 + Propagate type, ?M::0 : ?M::1 Assignment - ⊢ ?M3::0 ≈ Type M + ⊢ ?M::0 ≈ Type M Assumption 18 Failed to solve ⊢ Type M+1 ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type M+1 + ⊢ ?M::1 ≈ Type M+1 Assumption 19 Failed to solve ⊢ Type M+2 ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type M+2 + ⊢ ?M::1 ≈ Type M+2 Assumption 20 Failed to solve ⊢ Type M+3 ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type M+3 + ⊢ ?M::1 ≈ Type M+3 Assumption 21 Failed to solve ⊢ Type M ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type M + ⊢ ?M::1 ≈ Type M Assumption 22 Failed to solve ⊢ Type U ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type U + ⊢ ?M::1 ≈ Type U Assumption 23 Failed to solve ⊢ - (?M3::1 ≈ Type U+1) ⊕ - (?M3::1 ≈ Type U+2) ⊕ - (?M3::1 ≈ Type U+3) ⊕ - (?M3::1 ≈ Type M) ⊕ - (?M3::1 ≈ Type U) + (?M::1 ≈ Type U+1) ⊕ (?M::1 ≈ Type U+2) ⊕ (?M::1 ≈ Type U+3) ⊕ (?M::1 ≈ Type M) ⊕ (?M::1 ≈ Type U) Destruct/Decompose - ⊢ Type U+1 ≺ ?M3::1 - Propagate type, ?M3::0 : ?M3::1 + ⊢ Type U+1 ≺ ?M::1 + Propagate type, ?M::0 : ?M::1 Assignment - ⊢ ?M3::0 ≈ Type U + ⊢ ?M::0 ≈ Type U Assumption 24 Failed to solve ⊢ Type U+1 ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type U+1 + ⊢ ?M::1 ≈ Type U+1 Assumption 25 Failed to solve ⊢ Type U+2 ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type U+2 + ⊢ ?M::1 ≈ Type U+2 Assumption 26 Failed to solve ⊢ Type U+3 ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type U+3 + ⊢ ?M::1 ≈ Type U+3 Assumption 27 Failed to solve ⊢ Type M ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type M + ⊢ ?M::1 ≈ Type M Assumption 28 Failed to solve ⊢ Type U ≺ Type Substitution - ⊢ ?M3::1 ≺ Type + ⊢ ?M::1 ≺ Type (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of f::explicit with arguments: - ?M3::0 + ?M::0 Bool Bool Assignment - ⊢ ?M3::1 ≈ Type U + ⊢ ?M::1 ≈ Type U Assumption 29 Failed to solve -a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ a ≺ if (if a b ⊤) a ⊤ +a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ a ≺ if (if a b ⊤) a ⊤ Substitution - a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ a ≺ ?M3::5[lift:0:1] + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ a ≺ ?M::5[lift:0:1] Substitution - a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ ?M3::8 ≺ ?M3::5[lift:0:1] + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ ?M::8 ≺ ?M::5[lift:0:1] Destruct/Decompose - a : Bool, b : Bool, H : ?M3::2 ⊢ Π H_na : ?M3::7, ?M3::8 ≺ Π _ : ?M3::4, ?M3::5[lift:0:1] + a : Bool, b : Bool, H : ?M::2 ⊢ Π H_na : ?M::7, ?M::8 ≺ Π _ : ?M::4, ?M::5[lift:0:1] (line: 27: pos: 21) Type of argument 6 must be convertible to the expected type in the application of DisjCases::explicit with arguments: - ?M3::3 - ?M3::4 - ?M3::5 + ?M::3 + ?M::4 + ?M::5 EM a - λ H_a : ?M3::6, H - λ H_na : ?M3::7, NotImp1 (MT H H_na) + λ H_a : ?M::6, H + λ H_na : ?M::7, NotImp1 (MT H H_na) Assignment - a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ a ≈ ?M3::8 + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ a ≈ ?M::8 Destruct/Decompose - a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ if a b ⊤ ≈ if ?M3::8 ?M3::9 ⊤ + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ if a b ⊤ ≈ if ?M::8 ?M::9 ⊤ Normalize - a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ if a b ⊤ ≈ ?M3::8 ⇒ ?M3::9 + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ if a b ⊤ ≈ ?M::8 ⇒ ?M::9 Substitution - a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ if a b ⊤ ≈ ?M3::10 + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ if a b ⊤ ≈ ?M::10 Destruct/Decompose a : Bool, b : Bool, - H : ?M3::2, - H_na : ?M3::7 ⊢ - if (if a b ⊤) a ⊤ ≺ if ?M3::10 ?M3::11 ⊤ + H : ?M::2, + H_na : ?M::7 ⊢ + if (if a b ⊤) a ⊤ ≺ if ?M::10 ?M::11 ⊤ Normalize - a : Bool, - b : Bool, - H : ?M3::2, - H_na : ?M3::7 ⊢ - (a ⇒ b) ⇒ a ≺ if ?M3::10 ?M3::11 ⊤ + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ (a ⇒ b) ⇒ a ≺ if ?M::10 ?M::11 ⊤ Substitution a : Bool, b : Bool, - H : ?M3::2, - H_na : ?M3::7 ⊢ - ?M3::2[lift:0:2] ≺ if ?M3::10 ?M3::11 ⊤ + H : ?M::2, + H_na : ?M::7 ⊢ + ?M::2[lift:0:2] ≺ if ?M::10 ?M::11 ⊤ Normalize a : Bool, b : Bool, - H : ?M3::2, - H_na : ?M3::7 ⊢ - ?M3::2[lift:0:2] ≺ ?M3::10 ⇒ ?M3::11 + H : ?M::2, + H_na : ?M::7 ⊢ + ?M::2[lift:0:2] ≺ ?M::10 ⇒ ?M::11 (line: 29: pos: 48) Type of argument 3 must be convertible to the expected type in the application of MT::explicit with arguments: - ?M3::10 - ?M3::11 + ?M::10 + ?M::11 H H_na Normalize assignment - ?M3::0 + ?M::0 Assignment - a : Bool, b : Bool ⊢ ?M3::2 ≈ ?M3::0 + a : Bool, b : Bool ⊢ ?M::2 ≈ ?M::0 Destruct/Decompose a : Bool, b : Bool ⊢ - Π H : ?M3::2, ?M3::5 ≺ Π _ : ?M3::0, ?M3::1[lift:0:1] + Π H : ?M::2, ?M::5 ≺ Π _ : ?M::0, ?M::1[lift:0:1] (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of Discharge::explicit with arguments: - ?M3::0 - ?M3::1 - λ H : ?M3::2, + ?M::0 + ?M::1 + λ H : ?M::2, DisjCases (EM a) - (λ H_a : ?M3::6, H) - (λ H_na : ?M3::7, NotImp1 (MT H H_na)) + (λ H_a : ?M::6, H) + (λ H_na : ?M::7, NotImp1 (MT H H_na)) Assignment - a : Bool, b : Bool ⊢ ?M3::0 ≈ (a ⇒ b) ⇒ a + a : Bool, b : Bool ⊢ ?M::0 ≈ (a ⇒ b) ⇒ a Destruct/Decompose - a : Bool, b : Bool ⊢ ?M3::0 ⇒ ?M3::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a + a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a Destruct/Decompose a : Bool ⊢ - Π b : Bool, ?M3::0 ⇒ ?M3::1 ≺ + Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a Destruct/Decompose ⊢ - Π a b : Bool, ?M3::0 ⇒ ?M3::1 ≺ + Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type. Assignment - a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ ?M3::10 ≈ ?M3::8 ⇒ ?M3::9 + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ ?M::10 ≈ ?M::8 ⇒ ?M::9 Destruct/Decompose - a : Bool, b : Bool, H : ?M3::2, H_na : ?M3::7 ⊢ ¬ ?M3::10 ≺ ¬ (?M3::8 ⇒ ?M3::9) + a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ ¬ ?M::10 ≺ ¬ (?M::8 ⇒ ?M::9) (line: 29: pos: 40) Type of argument 3 must be convertible to the expected type in the application of NotImp1::explicit with arguments: - ?M3::8 - ?M3::9 + ?M::8 + ?M::9 MT H H_na Assignment - a : Bool, b : Bool, H : ?M3::2 ⊢ if (if a b ⊤) a ⊤ ≺ ?M3::5 + a : Bool, b : Bool, H : ?M::2 ⊢ if (if a b ⊤) a ⊤ ≺ ?M::5 Normalize - a : Bool, b : Bool, H : ?M3::2 ⊢ (a ⇒ b) ⇒ a ≺ ?M3::5 + a : Bool, b : Bool, H : ?M::2 ⊢ (a ⇒ b) ⇒ a ≺ ?M::5 Normalize - a : Bool, b : Bool, H : ?M3::2, H_a : ?M3::6 ⊢ (a ⇒ b) ⇒ a ≺ ?M3::5[lift:0:1] + a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ ?M::5[lift:0:1] Substitution - a : Bool, b : Bool, H : ?M3::2, H_a : ?M3::6 ⊢ ?M3::2[lift:0:2] ≺ ?M3::5[lift:0:1] + a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ ?M::2[lift:0:2] ≺ ?M::5[lift:0:1] Destruct/Decompose a : Bool, b : Bool, - H : ?M3::2 ⊢ - Π H_a : ?M3::6, ?M3::2[lift:0:2] ≺ Π _ : ?M3::3, ?M3::5[lift:0:1] + H : ?M::2 ⊢ + Π H_a : ?M::6, ?M::2[lift:0:2] ≺ Π _ : ?M::3, ?M::5[lift:0:1] (line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of DisjCases::explicit with arguments: - ?M3::3 - ?M3::4 - ?M3::5 + ?M::3 + ?M::4 + ?M::5 EM a - λ H_a : ?M3::6, H - λ H_na : ?M3::7, NotImp1 (MT H H_na) + λ H_a : ?M::6, H + λ H_na : ?M::7, NotImp1 (MT H H_na) Normalize assignment - ?M3::0 + ?M::0 Assignment - a : Bool, b : Bool ⊢ ?M3::2 ≈ ?M3::0 + a : Bool, b : Bool ⊢ ?M::2 ≈ ?M::0 Destruct/Decompose - a : Bool, b : Bool ⊢ Π H : ?M3::2, ?M3::5 ≺ Π _ : ?M3::0, ?M3::1[lift:0:1] + a : Bool, b : Bool ⊢ Π H : ?M::2, ?M::5 ≺ Π _ : ?M::0, ?M::1[lift:0:1] (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of Discharge::explicit with arguments: - ?M3::0 - ?M3::1 - λ H : ?M3::2, - DisjCases (EM a) (λ H_a : ?M3::6, H) (λ H_na : ?M3::7, NotImp1 (MT H H_na)) + ?M::0 + ?M::1 + λ H : ?M::2, + DisjCases (EM a) (λ H_a : ?M::6, H) (λ H_na : ?M::7, NotImp1 (MT H H_na)) Assignment - a : Bool, b : Bool ⊢ ?M3::0 ≈ (a ⇒ b) ⇒ a + a : Bool, b : Bool ⊢ ?M::0 ≈ (a ⇒ b) ⇒ a Destruct/Decompose - a : Bool, b : Bool ⊢ ?M3::0 ⇒ ?M3::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a + a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a Destruct/Decompose - a : Bool ⊢ Π b : Bool, ?M3::0 ⇒ ?M3::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a + a : Bool ⊢ Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a Destruct/Decompose - ⊢ Π a b : Bool, ?M3::0 ⇒ ?M3::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a + ⊢ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type. diff --git a/tests/lean/ex3.lean.expected.out b/tests/lean/ex3.lean.expected.out index c48adb645..7486c087d 100644 --- a/tests/lean/ex3.lean.expected.out +++ b/tests/lean/ex3.lean.expected.out @@ -7,19 +7,19 @@ myeq Bool ⊤ ⊥ Failed to solve ⊢ Bool ≺ T Substitution - ⊢ Bool ≺ ?M3::0 + ⊢ Bool ≺ ?M::0 (line: 5: pos: 6) Type of argument 2 must be convertible to the expected type in the application of myeq with arguments: - ?M3::0 + ?M::0 ⊤ a Assignment - ⊢ T ≺ ?M3::0 + ⊢ T ≺ ?M::0 (line: 5: pos: 6) Type of argument 3 must be convertible to the expected type in the application of myeq with arguments: - ?M3::0 + ?M::0 ⊤ a Assumed: myeq2 @@ -27,18 +27,18 @@ Failed to solve Failed to solve ⊢ Bool ≺ T Substitution - ⊢ Bool ≺ ?M3::0 + ⊢ Bool ≺ ?M::0 (line: 9: pos: 15) Type of argument 2 must be convertible to the expected type in the application of myeq2::explicit with arguments: - ?M3::0 + ?M::0 ⊤ a Assignment - ⊢ T ≺ ?M3::0 + ⊢ T ≺ ?M::0 (line: 9: pos: 15) Type of argument 3 must be convertible to the expected type in the application of myeq2::explicit with arguments: - ?M3::0 + ?M::0 ⊤ a diff --git a/tests/lean/let4.lean.expected.out b/tests/lean/let4.lean.expected.out index e5a2f6177..0e051e123 100644 --- a/tests/lean/let4.lean.expected.out +++ b/tests/lean/let4.lean.expected.out @@ -7,41 +7,41 @@ let a := 10, v1 := const a ⊤, v2 := v1 in v2 : vector Bool 10 let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2 let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2 : vector Bool 10 Failed to solve -a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ Bool ≈ ℤ +a : ℕ := 10, v1 : vector ?M::0 a := const a ⊤ ⊢ Bool ≈ ℤ Substitution - a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ ?M3::0[lift:0:1] ≈ ℤ + a : ℕ := 10, v1 : vector ?M::0 a := const a ⊤ ⊢ ?M::0[lift:0:1] ≈ ℤ Destruct/Decompose - a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ vector (?M3::0[lift:0:1]) a ≺ vector ℤ a + a : ℕ := 10, v1 : vector ?M::0 a := const a ⊤ ⊢ vector (?M::0[lift:0:1]) a ≺ vector ℤ a (line: 31: pos: 26) Type of definition 'v2' must be convertible to expected type. Assignment - a : ℕ := 10 ⊢ ?M3::0 ≈ Bool + a : ℕ := 10 ⊢ ?M::0 ≈ Bool Destruct/Decompose - a : ℕ := 10 ⊢ vector ?M3::0 a ≺ vector Bool a + a : ℕ := 10 ⊢ vector ?M::0 a ≺ vector Bool a (line: 30: pos: 26) Type of definition 'v1' must be convertible to expected type. Assumed: foo Coercion foo Failed to solve -a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ Bool ≈ ℤ +a : ℕ := 10, v1 : vector ?M::0 a := const a ⊤ ⊢ Bool ≈ ℤ Substitution - a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ ?M3::0[lift:0:1] ≈ ℤ + a : ℕ := 10, v1 : vector ?M::0 a := const a ⊤ ⊢ ?M::0[lift:0:1] ≈ ℤ Destruct/Decompose - a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ vector (?M3::0[lift:0:1]) a ≺ vector ℤ a + a : ℕ := 10, v1 : vector ?M::0 a := const a ⊤ ⊢ vector (?M::0[lift:0:1]) a ≺ vector ℤ a (line: 40: pos: 26) Type of definition 'v2' must be convertible to expected type. Assignment - a : ℕ := 10 ⊢ ?M3::0 ≈ Bool + a : ℕ := 10 ⊢ ?M::0 ≈ Bool Destruct/Decompose - a : ℕ := 10 ⊢ vector ?M3::0 a ≺ vector Bool a + a : ℕ := 10 ⊢ vector ?M::0 a ≺ vector Bool a (line: 39: pos: 26) Type of definition 'v1' must be convertible to expected type. Set: lean::pp::coercion Failed to solve -a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ Bool ≈ ℤ +a : ℕ := 10, v1 : vector ?M::0 a := const a ⊤ ⊢ Bool ≈ ℤ Substitution - a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ ?M3::0[lift:0:1] ≈ ℤ + a : ℕ := 10, v1 : vector ?M::0 a := const a ⊤ ⊢ ?M::0[lift:0:1] ≈ ℤ Destruct/Decompose - a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ vector (?M3::0[lift:0:1]) a ≺ vector ℤ a + a : ℕ := 10, v1 : vector ?M::0 a := const a ⊤ ⊢ vector (?M::0[lift:0:1]) a ≺ vector ℤ a (line: 48: pos: 26) Type of definition 'v2' must be convertible to expected type. Assignment - a : ℕ := 10 ⊢ ?M3::0 ≈ Bool + a : ℕ := 10 ⊢ ?M::0 ≈ Bool Destruct/Decompose - a : ℕ := 10 ⊢ vector ?M3::0 a ≺ vector Bool a + a : ℕ := 10 ⊢ vector ?M::0 a ≺ vector Bool a (line: 47: pos: 26) Type of definition 'v1' must be convertible to expected type. diff --git a/tests/lean/overload2.lean.expected.out b/tests/lean/overload2.lean.expected.out index 50d64e2c1..2d47031cd 100644 --- a/tests/lean/overload2.lean.expected.out +++ b/tests/lean/overload2.lean.expected.out @@ -1,107 +1,107 @@ Set: pp::colors Set: pp::unicode Failed to solve - ⊢ (?M3::0 ≈ Nat::add) ⊕ (?M3::0 ≈ Int::add) ⊕ (?M3::0 ≈ Real::add) + ⊢ (?M::0 ≈ Nat::add) ⊕ (?M::0 ≈ Int::add) ⊕ (?M::0 ≈ Real::add) (line: 1: pos: 10) Overloading at (Real::add | Int::add | Nat::add) 1 ⊤ Failed to solve ⊢ Bool ≺ ℕ Substitution - ⊢ Bool ≺ ?M3::8 + ⊢ Bool ≺ ?M::8 (line: 1: pos: 10) Type of argument 2 must be convertible to the expected type in the application of - ?M3::0 + ?M::0 with arguments: - ?M3::1 1 + ?M::1 1 ⊤ Assignment - ⊢ ℕ ≈ ?M3::8 + ⊢ ℕ ≈ ?M::8 Destruct/Decompose - ⊢ ℕ → ℕ ≈ Π x : ?M3::8, ?M3::9 x + ⊢ ℕ → ℕ ≈ Π x : ?M::8, ?M::9 x Substitution - ⊢ (?M3::7[inst:0 (?M3::1 1)]) (?M3::1 1) ≈ Π x : ?M3::8, ?M3::9 x + ⊢ (?M::7[inst:0 (?M::1 1)]) (?M::1 1) ≈ Π x : ?M::8, ?M::9 x (line: 1: pos: 10) Function expected at - ?M3::0 (?M3::1 1) ⊤ + ?M::0 (?M::1 1) ⊤ Assignment - _ : ℕ ⊢ λ x : ℕ, ℕ → ℕ ≈ ?M3::7 + _ : ℕ ⊢ λ x : ℕ, ℕ → ℕ ≈ ?M::7 Destruct/Decompose - _ : ℕ ⊢ ℕ → ℕ ≈ ?M3::7 _ + _ : ℕ ⊢ ℕ → ℕ ≈ ?M::7 _ Destruct/Decompose - ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M3::6, ?M3::7 x + ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 x Substitution - ⊢ ?M3::2 ≈ Π x : ?M3::6, ?M3::7 x + ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x (line: 1: pos: 10) Function expected at - ?M3::0 (?M3::1 1) ⊤ + ?M::0 (?M::1 1) ⊤ Assignment - ⊢ ℕ → ℕ → ℕ ≺ ?M3::2 - Propagate type, ?M3::0 : ?M3::2 + ⊢ ℕ → ℕ → ℕ ≺ ?M::2 + Propagate type, ?M::0 : ?M::2 Assignment - ⊢ ?M3::0 ≈ Nat::add + ⊢ ?M::0 ≈ Nat::add Assumption 0 Failed to solve ⊢ Bool ≺ ℤ Substitution - ⊢ Bool ≺ ?M3::8 + ⊢ Bool ≺ ?M::8 (line: 1: pos: 10) Type of argument 2 must be convertible to the expected type in the application of - ?M3::0 + ?M::0 with arguments: - ?M3::1 1 + ?M::1 1 ⊤ Assignment - ⊢ ℤ ≈ ?M3::8 + ⊢ ℤ ≈ ?M::8 Destruct/Decompose - ⊢ ℤ → ℤ ≈ Π x : ?M3::8, ?M3::9 x + ⊢ ℤ → ℤ ≈ Π x : ?M::8, ?M::9 x Substitution - ⊢ (?M3::7[inst:0 (?M3::1 1)]) (?M3::1 1) ≈ Π x : ?M3::8, ?M3::9 x + ⊢ (?M::7[inst:0 (?M::1 1)]) (?M::1 1) ≈ Π x : ?M::8, ?M::9 x (line: 1: pos: 10) Function expected at - ?M3::0 (?M3::1 1) ⊤ + ?M::0 (?M::1 1) ⊤ Assignment - _ : ℤ ⊢ λ x : ℤ, ℤ → ℤ ≈ ?M3::7 + _ : ℤ ⊢ λ x : ℤ, ℤ → ℤ ≈ ?M::7 Destruct/Decompose - _ : ℤ ⊢ ℤ → ℤ ≈ ?M3::7 _ + _ : ℤ ⊢ ℤ → ℤ ≈ ?M::7 _ Destruct/Decompose - ⊢ ℤ → ℤ → ℤ ≈ Π x : ?M3::6, ?M3::7 x + ⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::6, ?M::7 x Substitution - ⊢ ?M3::2 ≈ Π x : ?M3::6, ?M3::7 x + ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x (line: 1: pos: 10) Function expected at - ?M3::0 (?M3::1 1) ⊤ + ?M::0 (?M::1 1) ⊤ Assignment - ⊢ ℤ → ℤ → ℤ ≺ ?M3::2 - Propagate type, ?M3::0 : ?M3::2 + ⊢ ℤ → ℤ → ℤ ≺ ?M::2 + Propagate type, ?M::0 : ?M::2 Assignment - ⊢ ?M3::0 ≈ Int::add + ⊢ ?M::0 ≈ Int::add Assumption 2 Failed to solve ⊢ Bool ≺ ℝ Substitution - ⊢ Bool ≺ ?M3::8 + ⊢ Bool ≺ ?M::8 (line: 1: pos: 10) Type of argument 2 must be convertible to the expected type in the application of - ?M3::0 + ?M::0 with arguments: - ?M3::1 1 + ?M::1 1 ⊤ Assignment - ⊢ ℝ ≈ ?M3::8 + ⊢ ℝ ≈ ?M::8 Destruct/Decompose - ⊢ ℝ → ℝ ≈ Π x : ?M3::8, ?M3::9 x + ⊢ ℝ → ℝ ≈ Π x : ?M::8, ?M::9 x Substitution - ⊢ (?M3::7[inst:0 (?M3::1 1)]) (?M3::1 1) ≈ Π x : ?M3::8, ?M3::9 x + ⊢ (?M::7[inst:0 (?M::1 1)]) (?M::1 1) ≈ Π x : ?M::8, ?M::9 x (line: 1: pos: 10) Function expected at - ?M3::0 (?M3::1 1) ⊤ + ?M::0 (?M::1 1) ⊤ Assignment - _ : ℝ ⊢ λ x : ℝ, ℝ → ℝ ≈ ?M3::7 + _ : ℝ ⊢ λ x : ℝ, ℝ → ℝ ≈ ?M::7 Destruct/Decompose - _ : ℝ ⊢ ℝ → ℝ ≈ ?M3::7 _ + _ : ℝ ⊢ ℝ → ℝ ≈ ?M::7 _ Destruct/Decompose - ⊢ ℝ → ℝ → ℝ ≈ Π x : ?M3::6, ?M3::7 x + ⊢ ℝ → ℝ → ℝ ≈ Π x : ?M::6, ?M::7 x Substitution - ⊢ ?M3::2 ≈ Π x : ?M3::6, ?M3::7 x + ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x (line: 1: pos: 10) Function expected at - ?M3::0 (?M3::1 1) ⊤ + ?M::0 (?M::1 1) ⊤ Assignment - ⊢ ℝ → ℝ → ℝ ≺ ?M3::2 - Propagate type, ?M3::0 : ?M3::2 + ⊢ ℝ → ℝ → ℝ ≺ ?M::2 + Propagate type, ?M::0 : ?M::2 Assignment - ⊢ ?M3::0 ≈ Real::add + ⊢ ?M::0 ≈ Real::add Assumption 5 Assumed: R Assumed: T diff --git a/tests/lean/tst7.lean.expected.out b/tests/lean/tst7.lean.expected.out index 4207f5347..1947b4e7f 100644 --- a/tests/lean/tst7.lean.expected.out +++ b/tests/lean/tst7.lean.expected.out @@ -3,7 +3,7 @@ Assumed: f λ (A B : Type) (a : B), f B a Failed to solve -A : Type, a : ?M3::0, B : Type ⊢ ?M3::0[lift:0:2] ≺ B +A : Type, a : ?M::0, B : Type ⊢ ?M::0[lift:0:2] ≺ B (line: 4: pos: 40) Type of argument 2 must be convertible to the expected type in the application of f with arguments: diff --git a/tests/lean/tst9.lean.expected.out b/tests/lean/tst9.lean.expected.out index 4f27cbd26..0a66300da 100644 --- a/tests/lean/tst9.lean.expected.out +++ b/tests/lean/tst9.lean.expected.out @@ -5,9 +5,9 @@ Assumed: g Assumed: a Error (line: 5, pos: 6) type mismatch at application - g ⊤ (f ?M3::0 a a) + g ⊤ (f ?M::0 a a) Function type: N → N → Bool Arguments types: ⊤ : Bool - f ?M3::0 a a : ?M3::0 + f ?M::0 a a : ?M::0