michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/tests/lean/elab1.lean.expected.out

720 lines
31 KiB
Text
Raw Normal View History

Improve elaborator error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 20:21:57 +00:00
Set: pp::colors
Set: pp::unicode
Assumed: f
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
Failed to solve
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 18:16:22 +00:00
⊢ (?M::1 ≈ λ x : ℕ, x) ⊕ (?M::1 ≈ nat_to_int) ⊕ (?M::1 ≈ nat_to_real)
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
(line: 4: pos: 8) Coercion for
10
Failed to solve
⊢ Bool ≺ ℕ
Substitution
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 18:16:22 +00:00
⊢ Bool ≺ ?M::0
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
(line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
?M::1 10
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
⊤
Assignment
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 18:16:22 +00:00
⊢ ℕ ≺ ?M::0
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
Substitution
feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' This commit also simplifies the method check_pi in the type_checker and type_inferer. It also fixes process_meta_app in the elaborator. The problem was in the method process_meta_app and process_meta_inst. They were processing convertability constrains as equality constraints. For example, process_meta_app would handle ctx |- Type << ?f b as ctx |- Type =:= ?f b This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 20:25:00 +00:00
⊢ ?M::5[inst:0 (10)] ≺ ?M::0
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
(line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
?M::1 10
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
⊤
Assignment
feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' This commit also simplifies the method check_pi in the type_checker and type_inferer. It also fixes process_meta_app in the elaborator. The problem was in the method process_meta_app and process_meta_inst. They were processing convertability constrains as equality constraints. For example, process_meta_app would handle ctx |- Type << ?f b as ctx |- Type =:= ?f b This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 20:25:00 +00:00
x : ℕ ⊢ ℕ ≈ ?M::5
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
Destruct/Decompose
feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' This commit also simplifies the method check_pi in the type_checker and type_inferer. It also fixes process_meta_app in the elaborator. The problem was in the method process_meta_app and process_meta_inst. They were processing convertability constrains as equality constraints. For example, process_meta_app would handle ctx |- Type << ?f b as ctx |- Type =:= ?f b This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 20:25:00 +00:00
⊢ ℕ → ℕ ≈ Π x : ?M::4, ?M::5
Substitution
⊢ ?M::3 ≈ Π x : ?M::4, ?M::5
Function expected at
?M::1 10
Assignment
⊢ ℕ → ℕ ≺ ?M::3
Propagate type, ?M::1 : ?M::3
Assignment
⊢ ?M::1 ≈ λ x : ℕ, x
Assumption 0
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
Failed to solve
⊢ Bool ≺ ℤ
Substitution
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 18:16:22 +00:00
⊢ Bool ≺ ?M::0
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
(line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
?M::1 10
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
⊤
Assignment
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 18:16:22 +00:00
⊢ ℤ ≺ ?M::0
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
Substitution
feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' This commit also simplifies the method check_pi in the type_checker and type_inferer. It also fixes process_meta_app in the elaborator. The problem was in the method process_meta_app and process_meta_inst. They were processing convertability constrains as equality constraints. For example, process_meta_app would handle ctx |- Type << ?f b as ctx |- Type =:= ?f b This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 20:25:00 +00:00
⊢ ?M::5[inst:0 (10)] ≺ ?M::0
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
(line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
?M::1 10
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
⊤
Assignment
feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' This commit also simplifies the method check_pi in the type_checker and type_inferer. It also fixes process_meta_app in the elaborator. The problem was in the method process_meta_app and process_meta_inst. They were processing convertability constrains as equality constraints. For example, process_meta_app would handle ctx |- Type << ?f b as ctx |- Type =:= ?f b This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 20:25:00 +00:00
_ : ℕ ⊢ ℤ ≈ ?M::5
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
Destruct/Decompose
feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' This commit also simplifies the method check_pi in the type_checker and type_inferer. It also fixes process_meta_app in the elaborator. The problem was in the method process_meta_app and process_meta_inst. They were processing convertability constrains as equality constraints. For example, process_meta_app would handle ctx |- Type << ?f b as ctx |- Type =:= ?f b This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 20:25:00 +00:00
⊢ ℕ → ℤ ≈ Π x : ?M::4, ?M::5
Substitution
⊢ ?M::3 ≈ Π x : ?M::4, ?M::5
Function expected at
?M::1 10
Assignment
⊢ ℕ → ℤ ≺ ?M::3
Propagate type, ?M::1 : ?M::3
Assignment
⊢ ?M::1 ≈ nat_to_int
Assumption 1
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
Failed to solve
⊢ Bool ≺ ℝ
Substitution
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 18:16:22 +00:00
⊢ Bool ≺ ?M::0
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
(line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
?M::1 10
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
⊤
Assignment
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 18:16:22 +00:00
⊢ ℝ ≺ ?M::0
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
Substitution
feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' This commit also simplifies the method check_pi in the type_checker and type_inferer. It also fixes process_meta_app in the elaborator. The problem was in the method process_meta_app and process_meta_inst. They were processing convertability constrains as equality constraints. For example, process_meta_app would handle ctx |- Type << ?f b as ctx |- Type =:= ?f b This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 20:25:00 +00:00
⊢ ?M::5[inst:0 (10)] ≺ ?M::0
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
(line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
?M::1 10
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
⊤
Assignment
feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' This commit also simplifies the method check_pi in the type_checker and type_inferer. It also fixes process_meta_app in the elaborator. The problem was in the method process_meta_app and process_meta_inst. They were processing convertability constrains as equality constraints. For example, process_meta_app would handle ctx |- Type << ?f b as ctx |- Type =:= ?f b This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 20:25:00 +00:00
_ : ℕ ⊢ ℝ ≈ ?M::5
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
Destruct/Decompose
feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' This commit also simplifies the method check_pi in the type_checker and type_inferer. It also fixes process_meta_app in the elaborator. The problem was in the method process_meta_app and process_meta_inst. They were processing convertability constrains as equality constraints. For example, process_meta_app would handle ctx |- Type << ?f b as ctx |- Type =:= ?f b This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 20:25:00 +00:00
⊢ ℕ → ℝ ≈ Π x : ?M::4, ?M::5
Substitution
⊢ ?M::3 ≈ Π x : ?M::4, ?M::5
Function expected at
?M::1 10
Assignment
⊢ ℕ → ℝ ≺ ?M::3
Propagate type, ?M::1 : ?M::3
Assignment
⊢ ?M::1 ≈ nat_to_real
Assumption 2
Improve elaborator error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 20:21:57 +00:00
Assumed: g
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Error (line: 7, pos: 8) unexpected metavariable occurrence
Improve elaborator error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 20:21:57 +00:00
Assumed: h
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
Failed to solve
feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm' This commit also simplifies the method check_pi in the type_checker and type_inferer. It also fixes process_meta_app in the elaborator. The problem was in the method process_meta_app and process_meta_inst. They were processing convertability constrains as equality constraints. For example, process_meta_app would handle ctx |- Type << ?f b as ctx |- Type =:= ?f b This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 20:25:00 +00:00
x : ?M::0, A : Type ⊢ ?M::0 ≺ A
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
(line: 11: pos: 27) Type of argument 2 must be convertible to the expected type in the application of
h
with arguments:
A
x
refactor(equality): make homogeneous equality the default equality It was not a good idea to use heterogeneous equality as the default equality in Lean. It creates the following problems. - Heterogeneous equality does not propagate constraints in the elaborator. For example, suppose that l has type (List Int), then the expression l = nil will not propagate the type (List Int) to nil. - It is easy to write false. For example, suppose x has type Real, and the user writes x = 0. This is equivalent to false, since 0 has type Nat. The elaborator cannot introduce the coercion since x = 0 is a type correct expression. Homogeneous equality does not suffer from the problems above. We keep heterogeneous equality because it is useful for generating proof terms. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 23:20:02 +00:00
Assumed: my_eq
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
Failed to solve
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 18:16:22 +00:00
A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
(line: 15: pos: 51) Type of argument 2 must be convertible to the expected type in the application of
refactor(equality): make homogeneous equality the default equality It was not a good idea to use heterogeneous equality as the default equality in Lean. It creates the following problems. - Heterogeneous equality does not propagate constraints in the elaborator. For example, suppose that l has type (List Int), then the expression l = nil will not propagate the type (List Int) to nil. - It is easy to write false. For example, suppose x has type Real, and the user writes x = 0. This is equivalent to false, since 0 has type Nat. The elaborator cannot introduce the coercion since x = 0 is a type correct expression. Homogeneous equality does not suffer from the problems above. We keep heterogeneous equality because it is useful for generating proof terms. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 23:20:02 +00:00
my_eq
fix(tests/lean): adjust error messages in the expected output Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:08:35 +00:00
with arguments:
C
a
b
Improve elaborator error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-04 20:21:57 +00:00
Assumed: a
Assumed: b
Assumed: H
fix(library/elaborator): strength elaborator procedure for handling equality and convertability constraints This commit improves the condition for showing that an equality(and convertability) constraint cannot be solved. A nice consequence is that Lean produces nicer error messages. For example, the error message for unit test elab1.lean is more informative. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 21:04:26 +00:00
Failed to solve
feat(kernel/type_checker): provide the metavar_env to instantiate, it will minimize the number of local_entries needed Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 23:13:56 +00:00
⊢ if ?M::0 (if (if ?M::3 (if a ⊥ ⊤) ⊤) ⊥ ⊤) ⊤ ≺ b
fix(library/elaborator): strength elaborator procedure for handling equality and convertability constraints This commit improves the condition for showing that an equality(and convertability) constraint cannot be solved. A nice consequence is that Lean produces nicer error messages. For example, the error message for unit test elab1.lean is more informative. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 21:04:26 +00:00
Normalize
feat(kernel/type_checker): provide the metavar_env to instantiate, it will minimize the number of local_entries needed Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 23:13:56 +00:00
⊢ if ?M::0 (?M::3 ∧ a) ⊤ ≺ b
Substitution
⊢ if ?M::0 ?M::1 ⊤ ≺ b
Normalize
⊢ ?M::0 ⇒ ?M::1 ≺ b
(line: 20: pos: 18) Type of definition 't1' must be convertible to expected type.
Assignment
H1 : ?M::2 ⊢ ?M::3 ∧ a ≺ ?M::1
Substitution
H1 : ?M::2 ⊢ ?M::3 ∧ ?M::4 ≺ ?M::1
Destruct/Decompose
⊢ Π H1 : ?M::2, ?M::3 ∧ ?M::4 ≺ Π _ : ?M::0, ?M::1
(line: 20: pos: 18) Type of argument 3 must be convertible to the expected type in the application of
Discharge::explicit
with arguments:
?M::0
?M::1
λ H1 : ?M::2, Conj H1 (Conjunct1 H)
Assignment
H1 : ?M::2 ⊢ a ≺ ?M::4
Substitution
H1 : ?M::2 ⊢ ?M::5 ≺ ?M::4
(line: 20: pos: 37) Type of argument 4 must be convertible to the expected type in the application of
Conj::explicit
with arguments:
?M::3
?M::4
H1
Conjunct1 H
Assignment
H1 : ?M::2 ⊢ a ≈ ?M::5
Destruct/Decompose
H1 : ?M::2 ⊢ a ∧ b ≺ ?M::5 ∧ ?M::6
(line: 20: pos: 45) Type of argument 3 must be convertible to the expected type in the application of
Conjunct1::explicit
with arguments:
?M::5
?M::6
H
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ b ≈ a
fix(kernel/normalizer): do not apply substitutions in the normalizer It is incorrect to apply substitutions during normalization. The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 09:11:06 +00:00
Substitution
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 18:16:22 +00:00
⊢ b ≈ ?M::3
fix(kernel/normalizer): do not apply substitutions in the normalizer It is incorrect to apply substitutions during normalization. The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 09:11:06 +00:00
Destruct/Decompose
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 18:16:22 +00:00
⊢ b == b ≺ ?M::3 == ?M::4
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 22: pos: 22) Type of argument 6 must be convertible to the expected type in the application of
Trans::explicit
with arguments:
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 18:16:22 +00:00
?M::1
?M::2
?M::3
?M::4
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Refl a
Refl b
fix(kernel/normalizer): do not apply substitutions in the normalizer It is incorrect to apply substitutions during normalization. The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 09:11:06 +00:00
Assignment
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 18:16:22 +00:00
⊢ a ≈ ?M::3
fix(kernel/normalizer): do not apply substitutions in the normalizer It is incorrect to apply substitutions during normalization. The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 09:11:06 +00:00
Destruct/Decompose
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 18:16:22 +00:00
⊢ a == a ≺ ?M::2 == ?M::3
fix(kernel/normalizer): do not apply substitutions in the normalizer It is incorrect to apply substitutions during normalization. The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 09:11:06 +00:00
(line: 22: pos: 22) Type of argument 5 must be convertible to the expected type in the application of
Trans::explicit
with arguments:
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 18:16:22 +00:00
?M::1
?M::2
?M::3
?M::4
fix(kernel/normalizer): do not apply substitutions in the normalizer It is incorrect to apply substitutions during normalization. The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 09:11:06 +00:00
Refl a
Refl b
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
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 18:16:22 +00:00
⊢ (?M::0 ≈ Type) ⊕ (?M::0 ≈ Type 1) ⊕ (?M::0 ≈ Type 2) ⊕ (?M::0 ≈ Type M) ⊕ (?M::0 ≈ Type U)
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Destruct/Decompose
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 18:16:22 +00:00
⊢ Type ≺ ?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Failed to solve
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 18:16:22 +00:00
⊢ (?M::1 ≈ Type 1) ⊕ (?M::1 ≈ Type 2) ⊕ (?M::1 ≈ Type 3) ⊕ (?M::1 ≈ Type M) ⊕ (?M::1 ≈ Type U)
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Destruct/Decompose
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 18:16:22 +00:00
⊢ Type 1 ≺ ?M::1
Propagate type, ?M::0 : ?M::1
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Assignment
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 18:16:22 +00:00
⊢ ?M::0 ≈ Type
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type 1 ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type 1
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 1
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type 2 ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type 2
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 2
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type 3 ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type 3
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 3
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type M ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type M
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 4
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type U ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type U
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 5
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
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 18:16:22 +00:00
⊢ (?M::1 ≈ Type 2) ⊕ (?M::1 ≈ Type 3) ⊕ (?M::1 ≈ Type 4) ⊕ (?M::1 ≈ Type M) ⊕ (?M::1 ≈ Type U)
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Destruct/Decompose
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 18:16:22 +00:00
⊢ Type 2 ≺ ?M::1
Propagate type, ?M::0 : ?M::1
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Assignment
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 18:16:22 +00:00
⊢ ?M::0 ≈ Type 1
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 6
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type 2 ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type 2
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 7
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type 3 ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type 3
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 8
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type 4 ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type 4
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 9
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type M ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type M
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 10
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type U ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type U
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 11
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
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 18:16:22 +00:00
⊢ (?M::1 ≈ Type 3) ⊕ (?M::1 ≈ Type 4) ⊕ (?M::1 ≈ Type 5) ⊕ (?M::1 ≈ Type M) ⊕ (?M::1 ≈ Type U)
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Destruct/Decompose
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 18:16:22 +00:00
⊢ Type 3 ≺ ?M::1
Propagate type, ?M::0 : ?M::1
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Assignment
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 18:16:22 +00:00
⊢ ?M::0 ≈ Type 2
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 12
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type 3 ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type 3
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 13
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type 4 ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type 4
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 14
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type 5 ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type 5
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 15
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type M ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type M
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 16
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type U ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type U
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 17
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢
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 18:16:22 +00:00
(?M::1 ≈ Type M+1) ⊕ (?M::1 ≈ Type M+2) ⊕ (?M::1 ≈ Type M+3) ⊕ (?M::1 ≈ Type M) ⊕ (?M::1 ≈ Type U)
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Destruct/Decompose
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 18:16:22 +00:00
⊢ Type M+1 ≺ ?M::1
Propagate type, ?M::0 : ?M::1
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Assignment
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 18:16:22 +00:00
⊢ ?M::0 ≈ Type M
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 18
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type M+1 ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type M+1
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 19
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type M+2 ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type M+2
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 20
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type M+3 ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type M+3
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 21
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type M ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type M
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 22
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type U ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type U
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 23
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢
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 18:16:22 +00:00
(?M::1 ≈ Type U+1) ⊕ (?M::1 ≈ Type U+2) ⊕ (?M::1 ≈ Type U+3) ⊕ (?M::1 ≈ Type M) ⊕ (?M::1 ≈ Type U)
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Destruct/Decompose
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 18:16:22 +00:00
⊢ Type U+1 ≺ ?M::1
Propagate type, ?M::0 : ?M::1
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Assignment
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 18:16:22 +00:00
⊢ ?M::0 ≈ Type U
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 24
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type U+1 ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type U+1
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 25
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type U+2 ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type U+2
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 26
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type U+3 ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type U+3
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 27
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type M ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type M
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 28
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
⊢ Type U ≺ Type
Substitution
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 18:16:22 +00:00
⊢ ?M::1 ≺ Type
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
f::explicit
with arguments:
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 18:16:22 +00:00
?M::0
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Bool
Bool
Assignment
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 18:16:22 +00:00
⊢ ?M::1 ≈ Type U
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assumption 29
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Failed to solve
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 18:16:22 +00:00
a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ a ≺ if (if a b ⊤) a ⊤
feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition. Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P. For example, consider the constraint [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b)) Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet. So, the elaborator would continue to process the constraint, and convert it into: [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true Now, ?M::1 is assigned to the term if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true This is bad, since the original structure was lost. This commit also contains an example that only works after the commit is applied. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-29 17:14:54 +00:00
Normalize
a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ a ≺ (a ⇒ b) ⇒ a
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Substitution
feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition. Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P. For example, consider the constraint [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b)) Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet. So, the elaborator would continue to process the constraint, and convert it into: [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true Now, ?M::1 is assigned to the term if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true This is bad, since the original structure was lost. This commit also contains an example that only works after the commit is applied. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-29 17:14:54 +00:00
a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ a ≺ ?M::5[lift:0:1]
Substitution
a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ ?M::8 ≺ ?M::5[lift:0:1]
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Destruct/Decompose
feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition. Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P. For example, consider the constraint [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b)) Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet. So, the elaborator would continue to process the constraint, and convert it into: [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true Now, ?M::1 is assigned to the term if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true This is bad, since the original structure was lost. This commit also contains an example that only works after the commit is applied. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-29 17:14:54 +00:00
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:
?M::3
?M::4
?M::5
EM a
λ H_a : ?M::6, H
λ H_na : ?M::7, NotImp1 (MT H H_na)
Assignment
a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ a ≈ ?M::8
Destruct/Decompose
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 : ?M::2, H_na : ?M::7 ⊢ if a b ⊤ ≈ ?M::8 ⇒ ?M::9
Substitution
a : Bool, b : Bool, H : ?M::2, H_na : ?M::7 ⊢ if a b ⊤ ≈ ?M::10
Destruct/Decompose
a : Bool,
b : Bool,
H : ?M::2,
H_na : ?M::7 ⊢
if (if a b ⊤) a ⊤ ≺ if ?M::10 ?M::11 ⊤
Normalize
fix(kernel/normalizer): do not apply substitutions in the normalizer It is incorrect to apply substitutions during normalization. The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 09:11:06 +00:00
a : Bool,
b : Bool,
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 18:16:22 +00:00
H : ?M::2,
H_na : ?M::7 ⊢
feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition. Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P. For example, consider the constraint [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b)) Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet. So, the elaborator would continue to process the constraint, and convert it into: [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true Now, ?M::1 is assigned to the term if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true This is bad, since the original structure was lost. This commit also contains an example that only works after the commit is applied. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-29 17:14:54 +00:00
(a ⇒ b) ⇒ a ≺ if ?M::10 ?M::11 ⊤
Substitution
fix(kernel/normalizer): do not apply substitutions in the normalizer It is incorrect to apply substitutions during normalization. The problem is that we do not have support for tracking justifications in the normalizer. So, substitutions were being silently applied during normalization. Thus, the correctness of the conflict resolution in the elaboration was being affected. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 09:11:06 +00:00
a : Bool,
b : Bool,
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 18:16:22 +00:00
H : ?M::2,
H_na : ?M::7 ⊢
feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition. Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P. For example, consider the constraint [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b)) Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet. So, the elaborator would continue to process the constraint, and convert it into: [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true Now, ?M::1 is assigned to the term if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true This is bad, since the original structure was lost. This commit also contains an example that only works after the commit is applied. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-29 17:14:54 +00:00
?M::2[lift:0:2] ≺ if ?M::10 ?M::11 ⊤
Normalize
a : Bool,
b : Bool,
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:
?M::10
?M::11
H
H_na
Normalize assignment
?M::0
Assignment
a : Bool, b : Bool ⊢ ?M::2 ≈ ?M::0
fix(kernel/metavar): make sure the justification and substitution are always matching each other Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 09:39:52 +00:00
Destruct/Decompose
feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition. Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P. For example, consider the constraint [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b)) Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet. So, the elaborator would continue to process the constraint, and convert it into: [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true Now, ?M::1 is assigned to the term if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true This is bad, since the original structure was lost. This commit also contains an example that only works after the commit is applied. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-29 17:14:54 +00:00
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:
?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 ⊢ ?M::0 ≈ (a ⇒ b) ⇒ a
Destruct/Decompose
a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a
fix(kernel/metavar): make sure the justification and substitution are always matching each other Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 09:39:52 +00:00
Destruct/Decompose
feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition. Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P. For example, consider the constraint [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b)) Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet. So, the elaborator would continue to process the constraint, and convert it into: [a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true Now, ?M::1 is assigned to the term if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true This is bad, since the original structure was lost. This commit also contains an example that only works after the commit is applied. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-29 17:14:54 +00:00
a : Bool ⊢
Π b : Bool, ?M::0 ⇒ ?M::1 ≺
Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
Destruct/Decompose
⊢
Π 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 : ?M::2, H_na : ?M::7 ⊢ ?M::10 ≈ ?M::8 ⇒ ?M::9
Destruct/Decompose
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:
?M::8
?M::9
MT H H_na
Assignment
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 18:16:22 +00:00
a : Bool, b : Bool, H : ?M::2 ⊢ (a ⇒ b) ⇒ a ≺ ?M::5
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Normalize
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 18:16:22 +00:00
a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ ?M::5[lift:0:1]
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Substitution
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 18:16:22 +00:00
a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ ?M::2[lift:0:2] ≺ ?M::5[lift:0:1]
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
Destruct/Decompose
a : Bool,
b : Bool,
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 18:16:22 +00:00
H : ?M::2 ⊢
Π H_a : ?M::6, ?M::2[lift:0:2] ≺ Π _ : ?M::3, ?M::5[lift:0:1]
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
(line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of
DisjCases::explicit
with arguments:
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 18:16:22 +00:00
?M::3
?M::4
?M::5
feat(kernel): add unexpected_metavar_occurrence exception Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-25 02:56:44 +00:00
EM a
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 18:16:22 +00:00
λ H_a : ?M::6, H
λ H_na : ?M::7, NotImp1 (MT H H_na)
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Normalize assignment
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 18:16:22 +00:00
?M::0
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assignment
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 18:16:22 +00:00
a : Bool, b : Bool ⊢ ?M::2 ≈ ?M::0
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Destruct/Decompose
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 18:16:22 +00:00
a : Bool, b : Bool ⊢ Π H : ?M::2, ?M::5 ≺ Π _ : ?M::0, ?M::1[lift:0:1]
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
(line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
Discharge::explicit
with arguments:
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 18:16:22 +00:00
?M::0
?M::1
λ H : ?M::2,
DisjCases (EM a) (λ H_a : ?M::6, H) (λ H_na : ?M::7, NotImp1 (MT H H_na))
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Assignment
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 18:16:22 +00:00
a : Bool, b : Bool ⊢ ?M::0 ≈ (a ⇒ b) ⇒ a
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Destruct/Decompose
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 18:16:22 +00:00
a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Destruct/Decompose
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 18:16:22 +00:00
a : Bool ⊢ Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
Destruct/Decompose
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 18:16:22 +00:00
⊢ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
fix(kernel/metavar): add normalize assignment justification We need that when we normalize the assignment in a metavariable environment. That is, we replace metavariable in a substitution with other assignments. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-27 18:02:29 +00:00
(line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type.
Reference in a new issue Copy permalink