Commit 2018-09-05 11:51 97cd01b0
View on Github →refactor(linear_algebra/quotient_module): avoid using type class inference for setoids (#310)
Continuation of #212 . Avoid using type class inference for quotient modules, and introduce a version of quotient.mk specifically for quotient modules, whose output type is quotient β s rather than quotient (quotient_rel s), which should help type class inference.