Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-06-19 14:32 fbe1047b

View on Github →

feat(tactic/refine_struct): add refine_struct to use goal tags (#147)

Estimated changes

Modified algebra/pi_instances.lean

Modified category/basic.lean

added def mmap₂

Created data/dlist/basic.lean

added def dlist.join

Modified data/multiset.lean

Modified docs/tactics.md

Modified tactic/basic.lean

Modified tactic/interactive.lean