Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-03 16:58 956398c7

View on Github →

refactor(tactic/interactive): improve error reporting for simpa also make simpa fail on no goals or when applied where simp will work

Estimated changes

Modified algebra/gcd_domain.lean

Modified analysis/metric_space.lean

Modified analysis/topology/continuity.lean

Modified analysis/topology/topological_space.lean

Modified data/int/gcd.lean

Modified data/padics/padic_norm.lean

Modified data/rat.lean

modified theorem rat.denom_neg_eq_denom

modified theorem rat.num_denom_mk

modified theorem rat.num_zero

Modified data/real/nnreal.lean

Modified set_theory/ordinal.lean

Modified tactic/interactive.lean