lean2/tests/lean/open_tst.lean.expected.out

1 + 2 : ℕ
add : ?A → ?A → ?A
a + a : ℕ
a + a : ℕ
a + 1 : ℕ
a + a : ℕ
a + a : ℕ
a + 1 : ℕ
open_tst.lean:20:2: error: don't know how to synthesize placeholder

⊢ inhabited ℕ
open_tst.lean:20:2: error: failed to add declaration 'foo1' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
  ?M_1
a + a : ℕ
a + 1 : ℕ
open_tst.lean:29:2: error: don't know how to synthesize placeholder

⊢ inhabited ℕ
open_tst.lean:29:2: error: failed to add declaration 'foo2' to environment, value has metavariables
remark: set 'formatter.hide_full_terms' to false to see the complete term
  ?M_1
a + a : ℕ
-												feat(frontends/lean): add "except" notation for "open" command, allow multiple metaclasses to be opened in a single "open" command

											
										
										
											2015-02-11 19:02:59 +00:00
++ 2 : ℕ
-												fix(tests/lean): adjust remaining tests to changes in the standard library

											
										
										
											2015-10-14 01:35:16 +00:00
+								add : ?A → ?A → ?A
-												feat(frontends/lean): add "except" notation for "open" command, allow multiple metaclasses to be opened in a single "open" command

											
										
										
											2015-02-11 19:02:59 +00:00
+								a + a : ℕ
 								a + a : ℕ
-												fix(tests/lean): adjust remaining tests to changes in the standard library

											
										
										
											2015-10-14 01:35:16 +00:00
+								a + 1 : ℕ
-												feat(frontends/lean): add "except" notation for "open" command, allow multiple metaclasses to be opened in a single "open" command

											
										
										
											2015-02-11 19:02:59 +00:00
+								a + a : ℕ
 								a + a : ℕ
 								a + 1 : ℕ
-												fix(tests/lean): adjust remaining tests to changes in the standard library

											
										
										
											2015-10-14 01:35:16 +00:00
+								open_tst.lean:20:2: error: don't know how to synthesize placeholder
-												feat(frontends/lean): add "except" notation for "open" command, allow multiple metaclasses to be opened in a single "open" command

											
										
										
											2015-02-11 19:02:59 +00:00
 								⊢ inhabited ℕ
-												fix(tests/lean): adjust remaining tests to changes in the standard library

											
										
										
											2015-10-14 01:35:16 +00:00
+								open_tst.lean:20:2: error: failed to add declaration 'foo1' to environment, value has metavariables
-												feat(frontends/lean): hide subterms that do not contain metavariables
when generating "unresolved metavariables" error message

closes #473

											
										
										
											2015-03-13 19:42:57 +00:00
+								remark: set 'formatter.hide_full_terms' to false to see the complete term
-												feat(frontends/lean): add "except" notation for "open" command, allow multiple metaclasses to be opened in a single "open" command

											
										
										
											2015-02-11 19:02:59 +00:00
+								  ?M_1
 								a + a : ℕ
 								a + 1 : ℕ
-												fix(tests/lean): adjust remaining tests to changes in the standard library

											
										
										
											2015-10-14 01:35:16 +00:00
+								open_tst.lean:29:2: error: don't know how to synthesize placeholder
-												feat(frontends/lean): add "except" notation for "open" command, allow multiple metaclasses to be opened in a single "open" command

											
										
										
											2015-02-11 19:02:59 +00:00
 								⊢ inhabited ℕ
-												fix(tests/lean): adjust remaining tests to changes in the standard library

											
										
										
											2015-10-14 01:35:16 +00:00
+								open_tst.lean:29:2: error: failed to add declaration 'foo2' to environment, value has metavariables
-												feat(frontends/lean): hide subterms that do not contain metavariables
when generating "unresolved metavariables" error message

closes #473

											
										
										
											2015-03-13 19:42:57 +00:00
+								remark: set 'formatter.hide_full_terms' to false to see the complete term
-												feat(frontends/lean): add "except" notation for "open" command, allow multiple metaclasses to be opened in a single "open" command

											
										
										
											2015-02-11 19:02:59 +00:00
+								  ?M_1
-												fix(tests/lean): adjust remaining tests to changes in the standard library

											
										
										
											2015-10-14 01:35:16 +00:00
+								a + a : ℕ