Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-13 02:46 7cfc299f

View on Github →

refactor(tactic/interactive): minor cleanup, change ext notation

Estimated changes

Modified category/basic.lean

added def succeeds

added def try

Modified data/real/basic.lean

Modified docs/tactics.md

Modified tactic/basic.lean

Modified tactic/converter/old_conv.lean

Modified tactic/ext.lean

Modified tactic/replacer.lean