Commit 2022-08-01 10:42 2f1b3131
View on Github →chore(data/zmod): make zmod.int_cast_zmod_cast
@[norm_cast]
(#15753)
I was suprised that norm_cast
couldn't do anything with an expression including (((r : zmod 4) : ℤ) : zmod 4)
, turns out this lemma was missing a norm_cast
attribute.