Open monoidal opened 4 years ago
Maybe? Though we do want (p `MultMul` q) `MultMul` r)
to normalise to the same expression as p `MultMul` (q `MultMul r)
. And I'm not sure we can manage this with just reduceTyFamApp_maybe
, can we?
It depends on how smart we want Lint to be. More complex properties such as associativity could be just axioms and Core would have coercions witnessing them.
Fair enough. I don't have strong opinion either way.
Currently Core Lint manually reduces multiplication of multiplicities in
normalize
insideensureSubMult
. Goal: change toreduceTyFamApp_maybe
.