Mathlib v3 is deprecated. Go to Mathlib v4

Def a_to_quot

Modification history

2020-05-02 09:41
test/lint_coe_t.lean
fix(data/int/basic): use has_coe_t to prevent looping (#2573) …
Added a_to_quotView on Github →