PR #6061: feat(tactic/lint): linter for @[class] def

Stream: triage

[Random Issue Bot]

Today I chose PR 6061 for discussion!

feat(tactic/lint): linter for @[class] def
Created by @Mario Carneiro (@digama0) on 2021-02-05
Labels: mathport, merge-conflict, meta

Is this PR still relevant? Any recent updates? Anyone making progress?

[Mario Carneiro]

I'm updating this to current mathlib, but the issue with long typeclass inference of epi and mono persists. @Scott Morrison You had a plan to fix this?

[Scott Morrison]

I tried, but gave up. :-(

[Scott Morrison]

It was pretty involved. I can try again, but help appreciated from any category-theorists! The broken-in-many-places branch is at branch#epi_not_a_class. I've just merged master.