mathlib
685adb01 - fix(tactic/lint): allow pattern def (#7785)

Commit

4 years ago

fix(tactic/lint): allow pattern def (#7785) `Prop` sorted declarations are allowed to be `def` if they have the `@[pattern]` attribute

Author

fpvandoorn

Parents