Commit 2023-03-04 09:18 f2a5deba
View on Github →chore: address some porting notes mentioning congr
(#2595)
Switch to using congr!
instead, which is analogous to mathlib 3's congr'
.
chore: address some porting notes mentioning congr
(#2595)
Switch to using congr!
instead, which is analogous to mathlib 3's congr'
.