lean2/tests/lean/eq_class_error.lean.expected.out

eq_class_error.lean:15:10: error: don't know how to synthesize placeholder
decidable_eq_foo : Π f₁ f₂, decidable (f₁ = f₂)
⊢ decidable (b = b)
eq_class_error.lean:9:11: error: failed to synthesize placeholder

⊢ Π f₁ f₂,
    decidable (f₁ = f₂)
test(tests/lean/eq_class_error): save "workaround" for cryptic error message 2015-05-04 04:05:32 +00:00			`eq_class_error.lean:15:10: error: don't know how to synthesize placeholder`
chore(tests): mass-update for pp.binder_types false 2016-06-01 02:14:42 +00:00			`decidable_eq_foo : Π f₁ f₂, decidable (f₁ = f₂)`
test(tests/lean/eq_class_error): save "workaround" for cryptic error message 2015-05-04 04:05:32 +00:00			`⊢ decidable (b = b)`
			`eq_class_error.lean:9:11: error: failed to synthesize placeholder`

chore(tests): mass-update for pp.binder_types false 2016-06-01 02:14:42 +00:00			`⊢ Π f₁ f₂,`
test(tests/lean/eq_class_error): save "workaround" for cryptic error message 2015-05-04 04:05:32 +00:00			`decidable (f₁ = f₂)`