Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-24 14:22 e2c74215

View on Github →

feat(tactic/ext): new ext tactic and corresponding extensionality attribute

Estimated changes

Modified data/finset.lean

added theorem finset.ext'

Modified data/list/basic.lean

Modified data/multiset.lean

added theorem multiset.ext'

Modified data/set/basic.lean

Created data/stream/basic.lean

Modified docs/tactics.md

Modified tactic/interactive.lean

Modified tests/examples.lean