lean2/tests/lean/place_eqn.lean.expected.out

place_eqn.lean:4:18: error: don't know how to synthesize placeholder
foo : ℕ → ℕ
⊢ ℕ
place_eqn.lean:5:18: error: don't know how to synthesize placeholder
foo : ℕ → ℕ,
a : ℕ
⊢ ℕ
place_eqn.lean:3:11: error: failed to synthesize placeholder

⊢ ℕ → ℕ
-												feat(frontends/lean): ML-like notation for match and recursive equations

											
										
										
											2015-02-25 16:20:44 -08:00
+								place_eqn.lean:4:18: error: don't know how to synthesize placeholder
-												fix(frontends/lean/elaborator): solve placeholders before invoking equantions compiler

											
										
										
											2015-01-10 09:13:50 -08:00
+								foo : ℕ → ℕ
 								⊢ ℕ
-												feat(frontends/lean): ML-like notation for match and recursive equations

											
										
										
											2015-02-25 16:20:44 -08:00
+								place_eqn.lean:5:18: error: don't know how to synthesize placeholder
-												fix(frontends/lean/elaborator): solve placeholders before invoking equantions compiler

											
										
										
											2015-01-10 09:13:50 -08:00
+								foo : ℕ → ℕ,
 								a : ℕ
 								⊢ ℕ
-												perf(frontends/lean/elaborator): do not invoke recursive equation compiler when equations still contain metavariables

											
										
										
											2015-04-02 23:34:06 -07:00
+								place_eqn.lean:3:11: error: failed to synthesize placeholder
 								⊢ ℕ → ℕ