mathlib3
feat(tactic/linter): add decidable_classical linter
#2352
Merged
Overview
Commits
11
Changes
View On GitHub
Commits
  • feat(tactic/linter): add decidable_classical linter
    sgouezel committed 5 years ago
  • docstring
    sgouezel committed 5 years ago
  • cleanup
    sgouezel committed 5 years ago
  • fix build, cleanup
    sgouezel committed 5 years ago
  • fix test
    Scott Morrison committed 5 years ago
  • Update src/tactic/lint/type_classes.lean
    sgouezel committed 5 years ago
  • Update src/tactic/lint/type_classes.lean
    sgouezel committed 5 years ago
  • Update src/tactic/lint/default.lean
    sgouezel committed 5 years ago
  • Update src/tactic/lint/type_classes.lean
    sgouezel committed 5 years ago
  • Update src/data/dfinsupp.lean
    sgouezel committed 5 years ago
  • Merge branch 'master' into decidable_eq_linter
    mergify[bot] committed 5 years ago
FAQ Terms Privacy Refunds Impressum
Loading