Mathlib v3 is deprecated. Go to Mathlib v4

Theorem tactic.interactive.{u}

Modification history

2020-02-24 15:43
src/tactic/interactive.lean
feat(tactic/lint): support @[nolint unused_arguments] (#2041) …
Modified tactic.interactive.{u}View on Github →
2019-10-19 19:57
src/tactic/interactive.lean
feat(tactic/lint): rename and refactor sanity_check (#1556) …
Modified tactic.interactive.{u}View on Github →
2019-10-03 17:37
src/tactic/interactive.lean
chore(*): fix errors in library and sanity_check (#1499) …
Modified tactic.interactive.{u}View on Github →
2018-04-24 20:16
tactic/interactive.lean
feat(tactic/generalize_hyp): a version of `generalize` that also applies to assumptions (#110)
Added tactic.interactive.{u}View on Github →