mathlib
ad7519a3 - doc(tactic/lint): instructions on fails_quickly failure (#8910)

Commit

4 years ago

doc(tactic/lint): instructions on fails_quickly failure (#8910) * Also set `is_fast` to `tt`, since it takes ~10s on all of mathlib.

Author

fpvandoorn

Parents