Zulip Chat Archive

Stream: mathlib4

Topic: mathport simps translation


Johan Commelin (Dec 29 2022 at 11:16):

It looks like @Anatole Dedecker has to change @[simps symmApply] to @[simps symm_apply] over at https://github.com/leanprover-community/mathlib4/pull/1227/files/500bbd5d25cf08e5a40bd8c4abd78d982f9ae271..ef8b93e72e310ab742dcaa1c27dd4dc381c0e493#diff-0223a8e0343250fcee5149e859061c083c18f0f371a32b46c728a4807bc19263R42
It seems to me that mathport should be able to guess the right translation using its #align knowledge. Is this a bug?


Last updated: Dec 20 2023 at 11:08 UTC