Zulip Chat Archive

Stream: triage

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


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Mar 23 2021 at 00:32):

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?

view this post on Zulip Scott Morrison (Mar 23 2021 at 01:23):

I tried, but gave up. :-(

view this post on Zulip 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