Zulip Chat Archive

Stream: general

Topic: register_simp_attr

Yury G. Kudryashov (Jan 18 2023 at 07:12):

I've started porting Data.Nat.Parity, see https://github.com/leanprover-community/mathlib4/tree/port/Data.Nat.Parity

Yury G. Kudryashov (Jan 18 2023 at 07:12):

One of things that don't work is register_simp_attr parity_simps

Yury G. Kudryashov (Jan 18 2023 at 07:12):

Am I doing something wrong?

Yury G. Kudryashov (Jan 18 2023 at 07:18):

(I have most of the file ported)

Heather Macbeth (Jan 18 2023 at 07:18):

A common gotcha here is that the attribute needs to be in a different file from its uses. Is it that?

Last updated: Aug 03 2023 at 10:10 UTC