Commit 2021-02-05 12:11 34e366c6
View on Github →refactor(*): remove uses of @[class] def (#6028) Preparation for lean 4, which does not support this idiom.
refactor(*): remove uses of @[class] def (#6028) Preparation for lean 4, which does not support this idiom.