Documentation

Mathlib.Tactic.Lint

Linters for Mathlib #

In this file we define additional linters for mathlib.

Perhaps these should be moved to Std in the future.

Linter that checks whether a structure should be in Prop.

Instances For