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

refactor(kernel/metavar): avoid using unique names for default metavariable prefix

Browse source 
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 <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-07 10:16:22 -08:00
parent 2141ee12f4
commit 9c60eed93c
10 changed files with 298 additions and 314 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1043,7 +1043,7 @@ class pp_fn {
} }
result pp_metavar(expr const & a, unsigned depth) { 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)) { if (metavar_lctx(a)) {
format ctx_fmt; format ctx_fmt;
bool first = true; bool first = true;

5
src/kernel/metavar.cpp
View file

@ -50,8 +50,6 @@ public:
virtual expr const & get_main_expr() const { return m_expr; } 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) { void swap(metavar_env & a, metavar_env & b) {
swap(a.m_name_generator, b.m_name_generator); swap(a.m_name_generator, b.m_name_generator);
swap(a.m_metavar_data, b.m_metavar_data); swap(a.m_metavar_data, b.m_metavar_data);
@ -75,8 +73,9 @@ metavar_env::metavar_env(name const & prefix):
m_timestamp(0) { m_timestamp(0) {
} }
static name g_default_name("M");
metavar_env::metavar_env(): 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) { expr metavar_env::mk_metavar(context const & ctx, expr const & type) {

2
src/kernel/printer.cpp
View file

@ -76,7 +76,7 @@ struct print_expr_fn {
} }
void print_metavar(expr const & a, context const &) { void print_metavar(expr const & a, context const &) {
out() << "?M" << metavar_name(a); out() << "?" << metavar_name(a);
if (metavar_lctx(a)) { if (metavar_lctx(a)) {
out() << "["; out() << "[";
bool first = true; bool first = true;

2
src/tests/kernel/metavar.cpp
View file

@ -28,7 +28,7 @@ static std::ostream & operator<<(std::ostream & out, metavar_env const & menv) {
bool first = true; bool first = true;
menv.for_each_subst([&](name const & n, expr const & v) { menv.for_each_subst([&](name const & n, expr const & v) {
if (first) first = false; else out << "\n"; if (first) first = false; else out << "\n";
out << "?M" << n << " <- " << v; out << "?" << n << " <- " << v;
}); });
return out; return out;
} }

457
tests/lean/elab1.lean.expected.out
View file

@ -2,122 +2,122 @@
Set: pp::unicode Set: pp::unicode
Assumed: f Assumed: f
Failed to solve 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 (line: 4: pos: 8) Coercion for
10 10
Failed to solve Failed to solve
⊢ Bool ≺ ℕ ⊢ Bool ≺ ℕ
Substitution 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 (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
?M3::1 10 ?M::1 10
⊤ ⊤
Assignment Assignment
⊢ ℕ ≺ ?M3::0 ⊢ ℕ ≺ ?M::0
Substitution 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 (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
?M3::1 10 ?M::1 10
⊤ ⊤
Assignment Assignment
x : ℕ ⊢ λ x : ℕ, ℕ ≈ ?M3::5 x : ℕ ⊢ λ x : ℕ, ℕ ≈ ?M::5
Destruct/Decompose Destruct/Decompose
x : ℕ ⊢ ℕ ≈ ?M3::5 x x : ℕ ⊢ ℕ ≈ ?M::5 x
Destruct/Decompose Destruct/Decompose
⊢ ℕ → ℕ ≈ Π x : ?M3::4, ?M3::5 x ⊢ ℕ → ℕ ≈ Π x : ?M::4, ?M::5 x
Substitution Substitution
⊢ ?M3::3 ≈ Π x : ?M3::4, ?M3::5 x ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x
Function expected at Function expected at
?M3::1 10 ?M::1 10
Assignment Assignment
⊢ ℕ → ℕ ≺ ?M3::3 ⊢ ℕ → ℕ ≺ ?M::3
Propagate type, ?M3::1 : ?M3::3 Propagate type, ?M::1 : ?M::3
Assignment Assignment
⊢ ?M3::1 ≈ λ x : ℕ, x ⊢ ?M::1 ≈ λ x : ℕ, x
Assumption 0 Assumption 0
Failed to solve Failed to solve
⊢ Bool ≺ ℤ ⊢ Bool ≺ ℤ
Substitution 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 (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
?M3::1 10 ?M::1 10
⊤ ⊤
Assignment Assignment
⊢ ℤ ≺ ?M3::0 ⊢ ℤ ≺ ?M::0
Substitution 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 (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
?M3::1 10 ?M::1 10
⊤ ⊤
Assignment Assignment
_ : ℕ ⊢ λ x : ℕ, ℤ ≈ ?M3::5 _ : ℕ ⊢ λ x : ℕ, ℤ ≈ ?M::5
Destruct/Decompose Destruct/Decompose
_ : ℕ ⊢ ℤ ≈ ?M3::5 _ _ : ℕ ⊢ ℤ ≈ ?M::5 _
Destruct/Decompose Destruct/Decompose
⊢ ℕ → ℤ ≈ Π x : ?M3::4, ?M3::5 x ⊢ ℕ → ℤ ≈ Π x : ?M::4, ?M::5 x
Substitution Substitution
⊢ ?M3::3 ≈ Π x : ?M3::4, ?M3::5 x ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x
Function expected at Function expected at
?M3::1 10 ?M::1 10
Assignment Assignment
⊢ ℕ → ℤ ≺ ?M3::3 ⊢ ℕ → ℤ ≺ ?M::3
Propagate type, ?M3::1 : ?M3::3 Propagate type, ?M::1 : ?M::3
Assignment Assignment
⊢ ?M3::1 ≈ nat_to_int ⊢ ?M::1 ≈ nat_to_int
Assumption 1 Assumption 1
Failed to solve Failed to solve
⊢ Bool ≺ ℝ ⊢ Bool ≺ ℝ
Substitution 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 (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
?M3::1 10 ?M::1 10
⊤ ⊤
Assignment Assignment
⊢ ℝ ≺ ?M3::0 ⊢ ℝ ≺ ?M::0
Substitution 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 (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
?M3::1 10 ?M::1 10
⊤ ⊤
Assignment Assignment
_ : ℕ ⊢ λ x : ℕ, ℝ ≈ ?M3::5 _ : ℕ ⊢ λ x : ℕ, ℝ ≈ ?M::5
Destruct/Decompose Destruct/Decompose
_ : ℕ ⊢ ℝ ≈ ?M3::5 _ _ : ℕ ⊢ ℝ ≈ ?M::5 _
Destruct/Decompose Destruct/Decompose
⊢ ℕ → ℝ ≈ Π x : ?M3::4, ?M3::5 x ⊢ ℕ → ℝ ≈ Π x : ?M::4, ?M::5 x
Substitution Substitution
⊢ ?M3::3 ≈ Π x : ?M3::4, ?M3::5 x ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5 x
Function expected at Function expected at
?M3::1 10 ?M::1 10
Assignment Assignment
⊢ ℕ → ℝ ≺ ?M3::3 ⊢ ℕ → ℝ ≺ ?M::3
Propagate type, ?M3::1 : ?M3::3 Propagate type, ?M::1 : ?M::3
Assignment Assignment
⊢ ?M3::1 ≈ nat_to_real ⊢ ?M::1 ≈ nat_to_real
Assumption 2 Assumption 2
Assumed: g Assumed: g
Error (line: 7, pos: 8) unexpected metavariable occurrence Error (line: 7, pos: 8) unexpected metavariable occurrence
Assumed: h Assumed: h
Failed to solve 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 (line: 11: pos: 27) Type of argument 2 must be convertible to the expected type in the application of
h h
with arguments: with arguments:
@ -125,7 +125,7 @@ x : ?M3::0, A : Type ⊢ ?M3::0[lift:0:2] ≺ A
x x
Assumed: my_eq Assumed: my_eq
Failed to solve 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 (line: 15: pos: 51) Type of argument 2 must be convertible to the expected type in the application of
my_eq my_eq
with arguments: with arguments:
@ -139,557 +139,542 @@ Error (line: 20, pos: 28) unexpected metavariable occurrence
Failed to solve Failed to solve
⊢ b ≈ a ⊢ b ≈ a
Substitution Substitution
⊢ b ≈ ?M3::3 ⊢ b ≈ ?M::3
Destruct/Decompose 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 (line: 22: pos: 22) Type of argument 6 must be convertible to the expected type in the application of
Trans::explicit Trans::explicit
with arguments: with arguments:
?M3::1 ?M::1
?M3::2 ?M::2
?M3::3 ?M::3
?M3::4 ?M::4
Refl a Refl a
Refl b Refl b
Assignment Assignment
⊢ a ≈ ?M3::3 ⊢ a ≈ ?M::3
Destruct/Decompose 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 (line: 22: pos: 22) Type of argument 5 must be convertible to the expected type in the application of
Trans::explicit Trans::explicit
with arguments: with arguments:
?M3::1 ?M::1
?M3::2 ?M::2
?M3::3 ?M::3
?M3::4 ?M::4
Refl a Refl a
Refl b Refl b
Failed to solve 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 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 (line: 24: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Failed to solve Failed to solve
⊢ ⊢ (?M::1 ≈ Type 1) ⊕ (?M::1 ≈ Type 2) ⊕ (?M::1 ≈ Type 3) ⊕ (?M::1 ≈ Type M) ⊕ (?M::1 ≈ Type U)
(?M3::1 ≈ Type 1) ⊕ (?M3::1 ≈ Type 2) ⊕ (?M3::1 ≈ Type 3) ⊕ (?M3::1 ≈ Type M) ⊕ (?M3::1 ≈ Type U)
Destruct/Decompose Destruct/Decompose
⊢ Type 1 ≺ ?M3::1 ⊢ Type 1 ≺ ?M::1
Propagate type, ?M3::0 : ?M3::1 Propagate type, ?M::0 : ?M::1
Assignment Assignment
⊢ ?M3::0 ≈ Type ⊢ ?M::0 ≈ Type
Assumption 0 Assumption 0
Failed to solve Failed to solve
⊢ Type 1 ≺ Type ⊢ Type 1 ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type 1 ⊢ ?M::1 ≈ Type 1
Assumption 1 Assumption 1
Failed to solve Failed to solve
⊢ Type 2 ≺ Type ⊢ Type 2 ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type 2 ⊢ ?M::1 ≈ Type 2
Assumption 2 Assumption 2
Failed to solve Failed to solve
⊢ Type 3 ≺ Type ⊢ Type 3 ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type 3 ⊢ ?M::1 ≈ Type 3
Assumption 3 Assumption 3
Failed to solve Failed to solve
⊢ Type M ≺ Type ⊢ Type M ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type M ⊢ ?M::1 ≈ Type M
Assumption 4 Assumption 4
Failed to solve Failed to solve
⊢ Type U ≺ Type ⊢ Type U ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type U ⊢ ?M::1 ≈ Type U
Assumption 5 Assumption 5
Failed to solve Failed to solve
⊢ ⊢ (?M::1 ≈ Type 2) ⊕ (?M::1 ≈ Type 3) ⊕ (?M::1 ≈ Type 4) ⊕ (?M::1 ≈ Type M) ⊕ (?M::1 ≈ Type U)
(?M3::1 ≈ Type 2) ⊕ (?M3::1 ≈ Type 3) ⊕ (?M3::1 ≈ Type 4) ⊕ (?M3::1 ≈ Type M) ⊕ (?M3::1 ≈ Type U)
Destruct/Decompose Destruct/Decompose
⊢ Type 2 ≺ ?M3::1 ⊢ Type 2 ≺ ?M::1
Propagate type, ?M3::0 : ?M3::1 Propagate type, ?M::0 : ?M::1
Assignment Assignment
⊢ ?M3::0 ≈ Type 1 ⊢ ?M::0 ≈ Type 1
Assumption 6 Assumption 6
Failed to solve Failed to solve
⊢ Type 2 ≺ Type ⊢ Type 2 ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type 2 ⊢ ?M::1 ≈ Type 2
Assumption 7 Assumption 7
Failed to solve Failed to solve
⊢ Type 3 ≺ Type ⊢ Type 3 ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type 3 ⊢ ?M::1 ≈ Type 3
Assumption 8 Assumption 8
Failed to solve Failed to solve
⊢ Type 4 ≺ Type ⊢ Type 4 ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type 4 ⊢ ?M::1 ≈ Type 4
Assumption 9 Assumption 9
Failed to solve Failed to solve
⊢ Type M ≺ Type ⊢ Type M ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type M ⊢ ?M::1 ≈ Type M
Assumption 10 Assumption 10
Failed to solve Failed to solve
⊢ Type U ≺ Type ⊢ Type U ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type U ⊢ ?M::1 ≈ Type U
Assumption 11 Assumption 11
Failed to solve Failed to solve
⊢ ⊢ (?M::1 ≈ Type 3) ⊕ (?M::1 ≈ Type 4) ⊕ (?M::1 ≈ Type 5) ⊕ (?M::1 ≈ Type M) ⊕ (?M::1 ≈ Type U)
(?M3::1 ≈ Type 3) ⊕ (?M3::1 ≈ Type 4) ⊕ (?M3::1 ≈ Type 5) ⊕ (?M3::1 ≈ Type M) ⊕ (?M3::1 ≈ Type U)
Destruct/Decompose Destruct/Decompose
⊢ Type 3 ≺ ?M3::1 ⊢ Type 3 ≺ ?M::1
Propagate type, ?M3::0 : ?M3::1 Propagate type, ?M::0 : ?M::1
Assignment Assignment
⊢ ?M3::0 ≈ Type 2 ⊢ ?M::0 ≈ Type 2
Assumption 12 Assumption 12
Failed to solve Failed to solve
⊢ Type 3 ≺ Type ⊢ Type 3 ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type 3 ⊢ ?M::1 ≈ Type 3
Assumption 13 Assumption 13
Failed to solve Failed to solve
⊢ Type 4 ≺ Type ⊢ Type 4 ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type 4 ⊢ ?M::1 ≈ Type 4
Assumption 14 Assumption 14
Failed to solve Failed to solve
⊢ Type 5 ≺ Type ⊢ Type 5 ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type 5 ⊢ ?M::1 ≈ Type 5
Assumption 15 Assumption 15
Failed to solve Failed to solve
⊢ Type M ≺ Type ⊢ Type M ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type M ⊢ ?M::1 ≈ Type M
Assumption 16 Assumption 16
Failed to solve Failed to solve
⊢ Type U ≺ Type ⊢ Type U ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type U ⊢ ?M::1 ≈ Type U
Assumption 17 Assumption 17
Failed to solve Failed to solve
⊢ ⊢
(?M3::1 ≈ Type M+1) ⊕ (?M::1 ≈ Type M+1) ⊕ (?M::1 ≈ Type M+2) ⊕ (?M::1 ≈ Type M+3) ⊕ (?M::1 ≈ Type M) ⊕ (?M::1 ≈ Type U)
(?M3::1 ≈ Type M+2) ⊕
(?M3::1 ≈ Type M+3) ⊕
(?M3::1 ≈ Type M) ⊕
(?M3::1 ≈ Type U)
Destruct/Decompose Destruct/Decompose
⊢ Type M+1 ≺ ?M3::1 ⊢ Type M+1 ≺ ?M::1
Propagate type, ?M3::0 : ?M3::1 Propagate type, ?M::0 : ?M::1
Assignment Assignment
⊢ ?M3::0 ≈ Type M ⊢ ?M::0 ≈ Type M
Assumption 18 Assumption 18
Failed to solve Failed to solve
⊢ Type M+1 ≺ Type ⊢ Type M+1 ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type M+1 ⊢ ?M::1 ≈ Type M+1
Assumption 19 Assumption 19
Failed to solve Failed to solve
⊢ Type M+2 ≺ Type ⊢ Type M+2 ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type M+2 ⊢ ?M::1 ≈ Type M+2
Assumption 20 Assumption 20
Failed to solve Failed to solve
⊢ Type M+3 ≺ Type ⊢ Type M+3 ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type M+3 ⊢ ?M::1 ≈ Type M+3
Assumption 21 Assumption 21
Failed to solve Failed to solve
⊢ Type M ≺ Type ⊢ Type M ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type M ⊢ ?M::1 ≈ Type M
Assumption 22 Assumption 22
Failed to solve Failed to solve
⊢ Type U ≺ Type ⊢ Type U ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type U ⊢ ?M::1 ≈ Type U
Assumption 23 Assumption 23
Failed to solve Failed to solve
⊢ ⊢
(?M3::1 ≈ Type U+1) ⊕ (?M::1 ≈ Type U+1) ⊕ (?M::1 ≈ Type U+2) ⊕ (?M::1 ≈ Type U+3) ⊕ (?M::1 ≈ Type M) ⊕ (?M::1 ≈ Type U)
(?M3::1 ≈ Type U+2) ⊕
(?M3::1 ≈ Type U+3) ⊕
(?M3::1 ≈ Type M) ⊕
(?M3::1 ≈ Type U)
Destruct/Decompose Destruct/Decompose
⊢ Type U+1 ≺ ?M3::1 ⊢ Type U+1 ≺ ?M::1
Propagate type, ?M3::0 : ?M3::1 Propagate type, ?M::0 : ?M::1
Assignment Assignment
⊢ ?M3::0 ≈ Type U ⊢ ?M::0 ≈ Type U
Assumption 24 Assumption 24
Failed to solve Failed to solve
⊢ Type U+1 ≺ Type ⊢ Type U+1 ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type U+1 ⊢ ?M::1 ≈ Type U+1
Assumption 25 Assumption 25
Failed to solve Failed to solve
⊢ Type U+2 ≺ Type ⊢ Type U+2 ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type U+2 ⊢ ?M::1 ≈ Type U+2
Assumption 26 Assumption 26
Failed to solve Failed to solve
⊢ Type U+3 ≺ Type ⊢ Type U+3 ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type U+3 ⊢ ?M::1 ≈ Type U+3
Assumption 27 Assumption 27
Failed to solve Failed to solve
⊢ Type M ≺ Type ⊢ Type M ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type M ⊢ ?M::1 ≈ Type M
Assumption 28 Assumption 28
Failed to solve Failed to solve
⊢ Type U ≺ Type ⊢ Type U ≺ Type
Substitution 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 (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit f::explicit
with arguments: with arguments:
?M3::0 ?M::0
Bool Bool
Bool Bool
Assignment Assignment
⊢ ?M3::1 ≈ Type U ⊢ ?M::1 ≈ Type U
Assumption 29 Assumption 29
Failed to solve 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 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 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 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 (line: 27: pos: 21) Type of argument 6 must be convertible to the expected type in the application of
DisjCases::explicit DisjCases::explicit
with arguments: with arguments:
?M3::3 ?M::3
?M3::4 ?M::4
?M3::5 ?M::5
EM a EM a
λ H_a : ?M3::6, H λ H_a : ?M::6, H
λ H_na : ?M3::7, NotImp1 (MT H H_na) λ H_na : ?M::7, NotImp1 (MT H H_na)
Assignment 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 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 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 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 Destruct/Decompose
a : Bool, a : Bool,
b : Bool, b : Bool,
H : ?M3::2, H : ?M::2,
H_na : ?M3::7 ⊢ H_na : ?M::7 ⊢
if (if a b ⊤) a ⊤ ≺ if ?M3::10 ?M3::11 ⊤ if (if a b ⊤) a ⊤ ≺ if ?M::10 ?M::11 ⊤
Normalize Normalize
a : Bool, a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ (a ⇒ b) ⇒ a ≺ if ?M::10 ?M::11 ⊤
b : Bool,
H : ?M3::2,
H_na : ?M3::7 ⊢
(a ⇒ b) ⇒ a ≺ if ?M3::10 ?M3::11 ⊤
Substitution Substitution
a : Bool, a : Bool,
b : Bool, b : Bool,
H : ?M3::2, H : ?M::2,
H_na : ?M3::7 ⊢ H_na : ?M::7 ⊢
?M3::2[lift:0:2] ≺ if ?M3::10 ?M3::11 ⊤ ?M::2[lift:0:2] ≺ if ?M::10 ?M::11 ⊤
Normalize Normalize
a : Bool, a : Bool,
b : Bool, b : Bool,
H : ?M3::2, H : ?M::2,
H_na : ?M3::7 ⊢ H_na : ?M::7 ⊢
?M3::2[lift:0:2] ≺ ?M3::10 ⇒ ?M3::11 ?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 (line: 29: pos: 48) Type of argument 3 must be convertible to the expected type in the application of
MT::explicit MT::explicit
with arguments: with arguments:
?M3::10 ?M::10
?M3::11 ?M::11
H H
H_na H_na
Normalize assignment Normalize assignment
?M3::0 ?M::0
Assignment Assignment
a : Bool, b : Bool ⊢ ?M3::2 ≈ ?M3::0 a : Bool, b : Bool ⊢ ?M::2 ≈ ?M::0
Destruct/Decompose Destruct/Decompose
a : Bool, a : Bool,
b : 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 (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
Discharge::explicit Discharge::explicit
with arguments: with arguments:
?M3::0 ?M::0
?M3::1 ?M::1
λ H : ?M3::2, λ H : ?M::2,
DisjCases DisjCases
(EM a) (EM a)
(λ H_a : ?M3::6, H) (λ H_a : ?M::6, H)
(λ H_na : ?M3::7, NotImp1 (MT H H_na)) (λ H_na : ?M::7, NotImp1 (MT H H_na))
Assignment Assignment
a : Bool, b : Bool ⊢ ?M3::0 ≈ (a ⇒ b) ⇒ a a : Bool, b : Bool ⊢ ?M::0 ≈ (a ⇒ b) ⇒ a
Destruct/Decompose 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 Destruct/Decompose
a : Bool ⊢ a : Bool ⊢
Π b : Bool, ?M3::0 ⇒ ?M3::1 ≺ Π b : Bool, ?M::0 ⇒ ?M::1 ≺
Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
Destruct/Decompose Destruct/Decompose
⊢ ⊢
Π a b : Bool, ?M3::0 ⇒ ?M3::1 ≺ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺
Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
(line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type. (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type.
Assignment 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 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 (line: 29: pos: 40) Type of argument 3 must be convertible to the expected type in the application of
NotImp1::explicit NotImp1::explicit
with arguments: with arguments:
?M3::8 ?M::8
?M3::9 ?M::9
MT H H_na MT H H_na
Assignment 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 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 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 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 Destruct/Decompose
a : Bool, a : Bool,
b : Bool, b : Bool,
H : ?M3::2 ⊢ H : ?M::2 ⊢
Π H_a : ?M3::6, ?M3::2[lift:0:2] ≺ Π _ : ?M3::3, ?M3::5[lift:0:1] Π 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 (line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of
DisjCases::explicit DisjCases::explicit
with arguments: with arguments:
?M3::3 ?M::3
?M3::4 ?M::4
?M3::5 ?M::5
EM a EM a
λ H_a : ?M3::6, H λ H_a : ?M::6, H
λ H_na : ?M3::7, NotImp1 (MT H H_na) λ H_na : ?M::7, NotImp1 (MT H H_na)
Normalize assignment Normalize assignment
?M3::0 ?M::0
Assignment Assignment
a : Bool, b : Bool ⊢ ?M3::2 ≈ ?M3::0 a : Bool, b : Bool ⊢ ?M::2 ≈ ?M::0
Destruct/Decompose 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 (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
Discharge::explicit Discharge::explicit
with arguments: with arguments:
?M3::0 ?M::0
?M3::1 ?M::1
λ H : ?M3::2, λ H : ?M::2,
DisjCases (EM a) (λ H_a : ?M3::6, H) (λ H_na : ?M3::7, NotImp1 (MT H H_na)) DisjCases (EM a) (λ H_a : ?M::6, H) (λ H_na : ?M::7, NotImp1 (MT H H_na))
Assignment Assignment
a : Bool, b : Bool ⊢ ?M3::0 ≈ (a ⇒ b) ⇒ a a : Bool, b : Bool ⊢ ?M::0 ≈ (a ⇒ b) ⇒ a
Destruct/Decompose 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 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 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. (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type.

16
tests/lean/ex3.lean.expected.out
View file

@ -7,19 +7,19 @@ myeq Bool ⊤ ⊥
Failed to solve Failed to solve
⊢ Bool ≺ T ⊢ Bool ≺ T
Substitution 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 (line: 5: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
myeq myeq
with arguments: with arguments:
?M3::0 ?M::0
⊤ ⊤
a a
Assignment 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 (line: 5: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
myeq myeq
with arguments: with arguments:
?M3::0 ?M::0
⊤ ⊤
a a
Assumed: myeq2 Assumed: myeq2
@ -27,18 +27,18 @@ Failed to solve
Failed to solve Failed to solve
⊢ Bool ≺ T ⊢ Bool ≺ T
Substitution 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 (line: 9: pos: 15) Type of argument 2 must be convertible to the expected type in the application of
myeq2::explicit myeq2::explicit
with arguments: with arguments:
?M3::0 ?M::0
⊤ ⊤
a a
Assignment 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 (line: 9: pos: 15) Type of argument 3 must be convertible to the expected type in the application of
myeq2::explicit myeq2::explicit
with arguments: with arguments:
?M3::0 ?M::0
⊤ ⊤
a a

30
tests/lean/let4.lean.expected.out
View file

@ -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
let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2 : vector Bool 10 let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2 : vector Bool 10
Failed to solve Failed to solve
a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ Bool ≈ ℤ a : ℕ := 10, v1 : vector ?M::0 a := const a ⊤ ⊢ Bool ≈ ℤ
Substitution 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 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. (line: 31: pos: 26) Type of definition 'v2' must be convertible to expected type.
Assignment Assignment
a : ℕ := 10 ⊢ ?M3::0 ≈ Bool a : ℕ := 10 ⊢ ?M::0 ≈ Bool
Destruct/Decompose 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. (line: 30: pos: 26) Type of definition 'v1' must be convertible to expected type.
Assumed: foo Assumed: foo
Coercion foo Coercion foo
Failed to solve Failed to solve
a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ Bool ≈ ℤ a : ℕ := 10, v1 : vector ?M::0 a := const a ⊤ ⊢ Bool ≈ ℤ
Substitution 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 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. (line: 40: pos: 26) Type of definition 'v2' must be convertible to expected type.
Assignment Assignment
a : ℕ := 10 ⊢ ?M3::0 ≈ Bool a : ℕ := 10 ⊢ ?M::0 ≈ Bool
Destruct/Decompose 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. (line: 39: pos: 26) Type of definition 'v1' must be convertible to expected type.
Set: lean::pp::coercion Set: lean::pp::coercion
Failed to solve Failed to solve
a : ℕ := 10, v1 : vector ?M3::0 a := const a ⊤ ⊢ Bool ≈ ℤ a : ℕ := 10, v1 : vector ?M::0 a := const a ⊤ ⊢ Bool ≈ ℤ
Substitution 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 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. (line: 48: pos: 26) Type of definition 'v2' must be convertible to expected type.
Assignment Assignment
a : ℕ := 10 ⊢ ?M3::0 ≈ Bool a : ℕ := 10 ⊢ ?M::0 ≈ Bool
Destruct/Decompose 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. (line: 47: pos: 26) Type of definition 'v1' must be convertible to expected type.

92
tests/lean/overload2.lean.expected.out
View file

@ -1,107 +1,107 @@
Set: pp::colors Set: pp::colors
Set: pp::unicode Set: pp::unicode
Failed to solve 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 (line: 1: pos: 10) Overloading at
(Real::add | Int::add | Nat::add) 1 ⊤ (Real::add | Int::add | Nat::add) 1 ⊤
Failed to solve Failed to solve
⊢ Bool ≺ ℕ ⊢ Bool ≺ ℕ
Substitution 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 (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: with arguments:
?M3::1 1 ?M::1 1
⊤ ⊤
Assignment Assignment
⊢ ℕ ≈ ?M3::8 ⊢ ℕ ≈ ?M::8
Destruct/Decompose Destruct/Decompose
⊢ ℕ → ℕ ≈ Π x : ?M3::8, ?M3::9 x ⊢ ℕ → ℕ ≈ Π x : ?M::8, ?M::9 x
Substitution 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 (line: 1: pos: 10) Function expected at
?M3::0 (?M3::1 1) ⊤ ?M::0 (?M::1 1) ⊤
Assignment Assignment
_ : ℕ ⊢ λ x : ℕ, ℕ → ℕ ≈ ?M3::7 _ : ℕ ⊢ λ x : ℕ, ℕ → ℕ ≈ ?M::7
Destruct/Decompose Destruct/Decompose
_ : ℕ ⊢ ℕ → ℕ ≈ ?M3::7 _ _ : ℕ ⊢ ℕ → ℕ ≈ ?M::7 _
Destruct/Decompose Destruct/Decompose
⊢ ℕ → ℕ → ℕ ≈ Π x : ?M3::6, ?M3::7 x ⊢ ℕ → ℕ → ℕ ≈ Π x : ?M::6, ?M::7 x
Substitution Substitution
⊢ ?M3::2 ≈ Π x : ?M3::6, ?M3::7 x ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x
(line: 1: pos: 10) Function expected at (line: 1: pos: 10) Function expected at
?M3::0 (?M3::1 1) ⊤ ?M::0 (?M::1 1) ⊤
Assignment Assignment
⊢ ℕ → ℕ → ℕ ≺ ?M3::2 ⊢ ℕ → ℕ → ℕ ≺ ?M::2
Propagate type, ?M3::0 : ?M3::2 Propagate type, ?M::0 : ?M::2
Assignment Assignment
⊢ ?M3::0 ≈ Nat::add ⊢ ?M::0 ≈ Nat::add
Assumption 0 Assumption 0
Failed to solve Failed to solve
⊢ Bool ≺ ℤ ⊢ Bool ≺ ℤ
Substitution 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 (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: with arguments:
?M3::1 1 ?M::1 1
⊤ ⊤
Assignment Assignment
⊢ ℤ ≈ ?M3::8 ⊢ ℤ ≈ ?M::8
Destruct/Decompose Destruct/Decompose
⊢ ℤ → ℤ ≈ Π x : ?M3::8, ?M3::9 x ⊢ ℤ → ℤ ≈ Π x : ?M::8, ?M::9 x
Substitution 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 (line: 1: pos: 10) Function expected at
?M3::0 (?M3::1 1) ⊤ ?M::0 (?M::1 1) ⊤
Assignment Assignment
_ : ℤ ⊢ λ x : ℤ, ℤ → ℤ ≈ ?M3::7 _ : ℤ ⊢ λ x : ℤ, ℤ → ℤ ≈ ?M::7
Destruct/Decompose Destruct/Decompose
_ : ℤ ⊢ ℤ → ℤ ≈ ?M3::7 _ _ : ℤ ⊢ ℤ → ℤ ≈ ?M::7 _
Destruct/Decompose Destruct/Decompose
⊢ ℤ → ℤ → ℤ ≈ Π x : ?M3::6, ?M3::7 x ⊢ ℤ → ℤ → ℤ ≈ Π x : ?M::6, ?M::7 x
Substitution Substitution
⊢ ?M3::2 ≈ Π x : ?M3::6, ?M3::7 x ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x
(line: 1: pos: 10) Function expected at (line: 1: pos: 10) Function expected at
?M3::0 (?M3::1 1) ⊤ ?M::0 (?M::1 1) ⊤
Assignment Assignment
⊢ ℤ → ℤ → ℤ ≺ ?M3::2 ⊢ ℤ → ℤ → ℤ ≺ ?M::2
Propagate type, ?M3::0 : ?M3::2 Propagate type, ?M::0 : ?M::2
Assignment Assignment
⊢ ?M3::0 ≈ Int::add ⊢ ?M::0 ≈ Int::add
Assumption 2 Assumption 2
Failed to solve Failed to solve
⊢ Bool ≺ ℝ ⊢ Bool ≺ ℝ
Substitution 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 (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: with arguments:
?M3::1 1 ?M::1 1
⊤ ⊤
Assignment Assignment
⊢ ℝ ≈ ?M3::8 ⊢ ℝ ≈ ?M::8
Destruct/Decompose Destruct/Decompose
⊢ ℝ → ℝ ≈ Π x : ?M3::8, ?M3::9 x ⊢ ℝ → ℝ ≈ Π x : ?M::8, ?M::9 x
Substitution 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 (line: 1: pos: 10) Function expected at
?M3::0 (?M3::1 1) ⊤ ?M::0 (?M::1 1) ⊤
Assignment Assignment
_ : ℝ ⊢ λ x : ℝ, ℝ → ℝ ≈ ?M3::7 _ : ℝ ⊢ λ x : ℝ, ℝ → ℝ ≈ ?M::7
Destruct/Decompose Destruct/Decompose
_ : ℝ ⊢ ℝ → ℝ ≈ ?M3::7 _ _ : ℝ ⊢ ℝ → ℝ ≈ ?M::7 _
Destruct/Decompose Destruct/Decompose
⊢ ℝ → ℝ → ℝ ≈ Π x : ?M3::6, ?M3::7 x ⊢ ℝ → ℝ → ℝ ≈ Π x : ?M::6, ?M::7 x
Substitution Substitution
⊢ ?M3::2 ≈ Π x : ?M3::6, ?M3::7 x ⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x
(line: 1: pos: 10) Function expected at (line: 1: pos: 10) Function expected at
?M3::0 (?M3::1 1) ⊤ ?M::0 (?M::1 1) ⊤
Assignment Assignment
⊢ ℝ → ℝ → ℝ ≺ ?M3::2 ⊢ ℝ → ℝ → ℝ ≺ ?M::2
Propagate type, ?M3::0 : ?M3::2 Propagate type, ?M::0 : ?M::2
Assignment Assignment
⊢ ?M3::0 ≈ Real::add ⊢ ?M::0 ≈ Real::add
Assumption 5 Assumption 5
Assumed: R Assumed: R
Assumed: T Assumed: T

2
tests/lean/tst7.lean.expected.out
View file

@ -3,7 +3,7 @@
Assumed: f Assumed: f
λ (A B : Type) (a : B), f B a λ (A B : Type) (a : B), f B a
Failed to solve 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 (line: 4: pos: 40) Type of argument 2 must be convertible to the expected type in the application of
f f
with arguments: with arguments:

4
tests/lean/tst9.lean.expected.out
View file

@ -5,9 +5,9 @@
Assumed: g Assumed: g
Assumed: a Assumed: a
Error (line: 5, pos: 6) type mismatch at application Error (line: 5, pos: 6) type mismatch at application
g ⊤ (f ?M3::0 a a) g ⊤ (f ?M::0 a a)
Function type: Function type:
N → N → Bool N → N → Bool
Arguments types: Arguments types:
⊤ : Bool ⊤ : Bool
f ?M3::0 a a : ?M3::0 f ?M::0 a a : ?M::0