Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-10 15:54 f7654b3f

View on Github →

feat(tactic/generalizes): tactic for generalizing over multiple expressions (#2982) This commit adds a tactic generalizes which works like generalize but for multiple expressions at once. The tactic is more powerful than calling generalize multiple times since this usually fails when there are dependencies between the expressions. By contrast, generalizes handles at least some such situations.

Estimated changes

added inductive Vec.eq
added theorem Vec.eq_cons_inversion
added inductive Vec.fancy_unit
added theorem Vec.test₁
added theorem Vec.test₂
added inductive Vec
added theorem example_from_docs₁
added theorem example_from_docs₂