Commit 2020-05-02 09:41 06bae3e1

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.