mathlib3
e5c77892 - fix(lint/type_classes): fix instance_priority bug (#6305)

Commit

4 years ago

fix(lint/type_classes): fix instance_priority bug (#6305) The linter now doesn't fail if the type is a beta redex

Author

fpvandoorn

Parents