mathlib3
34e366c6 - refactor(*): remove uses of @[class] def (#6028)

Commit

5 years ago

refactor(*): remove uses of @[class] def (#6028) Preparation for lean 4, which does not support this idiom.

Author

digama0

Parents