lean2/tests/lean/extra/597b.hlean

-- open equiv
constants (A B : Type₀) (f : A ≃ B)
definition foo : A → B := f -- should fail
feat(hott): replace assert by have and merge namespace equiv.ops into equiv The coercion A ≃ B -> (A -> B) is now in namespace equiv. The notation ⁻¹ for symmetry of equivalences is not supported anymore. Use ⁻¹ᵉ 2016-03-03 15:48:27 +00:00			`-- open equiv`
test(tests/lean/extra): add test for issue #597 2015-05-13 22:26:13 +00:00			`constants (A B : Type₀) (f : A ≃ B)`
			`definition foo : A → B := f -- should fail`