Commit 2020-05-02 09:41 06bae3e1
View on Github →fix(data/int/basic): use has_coe_t to prevent looping (#2573)
The file src/computability/partrec.lean
no longer opens in vscode because type-class search times out. This happens because we have the instance has_coe ℤ α
which causes non-termination because coercions are chained transitively (has_coe ℤ ℤ
, has_coe ℤ ℤ
, ...). Even if the coercions would not apply to integers (and maybe avoid non-termination), it would still enumerate all 0,1,+,-
structures, of which there are unfortunately very many.
This PR therefore downgrades such instances to has_coe_t
to prevent non-termination due to transitivity. It also adds a linter to prevent this kind of error in the future.