lean2/tests/lean/overload2.lean.expected.out
Leonardo de Moura 9c60eed93c 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 <leonardo@microsoft.com>
2013-11-07 10:16:25 -08:00

121 lines
5.4 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

Set: pp::colors
Set: pp::unicode
Failed to solve
⊢ (?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 ≺ ?M::8
(line: 1: pos: 10) Type of argument 2 must be convertible to the expected type in the application of
?M::0
with arguments:
?M::1 1
Assignment
≈ ?M::8
Destruct/Decompose
≈ Π x : ?M::8, ?M::9 x
Substitution
⊢ (?M::7[inst:0 (?M::1 1)]) (?M::1 1) ≈ Π x : ?M::8, ?M::9 x
(line: 1: pos: 10) Function expected at
?M::0 (?M::1 1)
Assignment
_ : ⊢ λ x : , ≈ ?M::7
Destruct/Decompose
_ : ≈ ?M::7 _
Destruct/Decompose
≈ Π x : ?M::6, ?M::7 x
Substitution
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x
(line: 1: pos: 10) Function expected at
?M::0 (?M::1 1)
Assignment
≺ ?M::2
Propagate type, ?M::0 : ?M::2
Assignment
⊢ ?M::0 ≈ Nat::add
Assumption 0
Failed to solve
⊢ Bool ≺
Substitution
⊢ Bool ≺ ?M::8
(line: 1: pos: 10) Type of argument 2 must be convertible to the expected type in the application of
?M::0
with arguments:
?M::1 1
Assignment
≈ ?M::8
Destruct/Decompose
≈ Π x : ?M::8, ?M::9 x
Substitution
⊢ (?M::7[inst:0 (?M::1 1)]) (?M::1 1) ≈ Π x : ?M::8, ?M::9 x
(line: 1: pos: 10) Function expected at
?M::0 (?M::1 1)
Assignment
_ : ⊢ λ x : , ≈ ?M::7
Destruct/Decompose
_ : ≈ ?M::7 _
Destruct/Decompose
≈ Π x : ?M::6, ?M::7 x
Substitution
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x
(line: 1: pos: 10) Function expected at
?M::0 (?M::1 1)
Assignment
≺ ?M::2
Propagate type, ?M::0 : ?M::2
Assignment
⊢ ?M::0 ≈ Int::add
Assumption 2
Failed to solve
⊢ Bool ≺
Substitution
⊢ Bool ≺ ?M::8
(line: 1: pos: 10) Type of argument 2 must be convertible to the expected type in the application of
?M::0
with arguments:
?M::1 1
Assignment
≈ ?M::8
Destruct/Decompose
≈ Π x : ?M::8, ?M::9 x
Substitution
⊢ (?M::7[inst:0 (?M::1 1)]) (?M::1 1) ≈ Π x : ?M::8, ?M::9 x
(line: 1: pos: 10) Function expected at
?M::0 (?M::1 1)
Assignment
_ : ⊢ λ x : , ≈ ?M::7
Destruct/Decompose
_ : ≈ ?M::7 _
Destruct/Decompose
≈ Π x : ?M::6, ?M::7 x
Substitution
⊢ ?M::2 ≈ Π x : ?M::6, ?M::7 x
(line: 1: pos: 10) Function expected at
?M::0 (?M::1 1)
Assignment
≺ ?M::2
Propagate type, ?M::0 : ?M::2
Assignment
⊢ ?M::0 ≈ Real::add
Assumption 5
Assumed: R
Assumed: T
Assumed: r2t
Coercion r2t
Assumed: t2r
Coercion t2r
Assumed: f
Assumed: a
Assumed: b
Set: lean::pp::coercion
Set: lean::pp::notation
f a b
f (r2t b) (t2r a)
Assumed: g
f a b
f (r2t b) (t2r a)