Categorical structure of Quiv

Stream: PR reviews

[Robert Maxton]

Am starting to PR my ongoing work on the categorical structure of Quiv. I've run into trouble early, though:
https://github.com/leanprover-community/mathlib4/compare/robertmaxton42/quiv-helper1

The simpNF linter claims that some of these lemmas can be proven with simp, but when I actually try it in my local copy it doesn't work. Can I get some advice fixing this?

[Robert Maxton]

#23989 isn't even getting to the lint and build stage; I'm getting Error: Unhandled error: HttpError: Resource not accessible by integration

[Ruben Van de Velde]

That's because it comes from a fork - we don't support that, I'm afraid

[Robert Maxton]

... Oh dammit, I thought I'd removed that -_-

[Robert Maxton]

Thanks for the tip