Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-11 13:43 176852df

View on Github →

feat(tactic/lint): check if inhabited instances should be nonempty (#1971)

  • add inhabited vs nonempty linter
  • add new linter to ci
  • start updating files to pass linter
  • more linter fixes
  • fix more linter errors
  • more fixes
  • fix build
  • remove unnecessary instances
  • nicer proof
  • adjust inhabit tactic
  • improve proof
  • move instance to better place
  • generalize instance
  • fix build
  • inhabited -> nonempty
  • fix build

Estimated changes

modified theorem list.func.get_neg
modified theorem set.empty_ne_univ
modified theorem set.Inter_const
modified theorem set.Inter_inter
modified theorem set.Union_const
modified theorem set.Union_union
modified theorem set.diff_Union
modified theorem set.inter_Inter
modified theorem set.union_Union
modified theorem constr_range
modified theorem exists_const
modified theorem forall_const
modified theorem filter.prod_map_at_top_eq
modified theorem emetric.cauchy_seq_iff'
modified theorem emetric.cauchy_seq_iff
modified theorem emetric.tendsto_at_top
modified theorem cauchy_seq_iff_tendsto
modified theorem cauchy_seq_of_controlled