Commit 2023-03-22 20:21 1b8e1c63
View on Github →feat: support and improve notation_class in simps (#2883)
- If you write
@[simps]
for the definition of anAddGroup
, it will now generate the correct lemmas for0
,+
,nsmul
andzsmul
usingOfNat
and heterogenous operations. This is needed for #2609.- This is a lot more flexible than the Lean 3 implementation, in order to handle
nsmul
,zsmul
and numerals. - It doesn't handle the
zpow
andnpow
projections, since their argument order is different than that ofHPow.pow
(that was likely done for the sake ofto_additive
, but we can consider to revisit that choice).
- This is a lot more flexible than the Lean 3 implementation, in order to handle
- Also fixes the
nvMonoid
bug encountered in #2609- There was an issue where the wrong projection was chosen, since
toDiv
is a prefix oftoDivInvMonoid
- Before we were checking if
_toDiv
is a prefix of your projection with_
prepended (e.g._toDivInvMonoid
), now we are checking whethertoDiv_
is a prefix of your projection with_
appended (which doesn't matchtoDivInvMonoid_
).
- There was an issue where the wrong projection was chosen, since