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.