declaration linter

Stream: general

[Reid Barton]

I wrote a "declaration linter" that processes each declaration and checks for things that look dodgy.
Currently, it looks for lemmas whose type is not a Prop, and structures/classes which could be Props but aren't.
Here's the output on the core library and (a slightly out-of-date) mathlib: https://gist.github.com/rwbarton/4e119ba9b812debac08c8a54afb104bd

[Reid Barton]

I want to add warnings for unused variables next, but that will be a bit more difficult.

[Reid Barton]

Hmm, some of the output is duplicated--not sure why

[Reid Barton]

Start at line 141

[Reid Barton]

Ah, I figured out why--some leftover testing code.