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