Commit 2023-10-14 13:46 04245a84
View on Github →chore: remove autoImplicit in NeZero.lean (#7673) I was unaware there was some of these still lying around - should we tidy these up?
chore: remove autoImplicit in NeZero.lean (#7673) I was unaware there was some of these still lying around - should we tidy these up?