Random Issue Bot (Mar 20 2021 at 14:26):
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 (Mar 23 2021 at 00:32):
I'm updating this to current mathlib, but the issue with long typeclass inference of
mono persists. @Scott Morrison You had a plan to fix this?
Scott Morrison (Mar 23 2021 at 01:23):
I tried, but gave up. :-(
Scott Morrison (Mar 23 2021 at 01:26):
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.
Last updated: May 09 2021 at 16:20 UTC