Mathlib v3 is deprecated. Go to Mathlib v4

Def tactic.interactive.normed_a

Modification history

2020-03-22 17:01
src/tactic/norm_num.lean
feat(tactic/doc_commands): allow doc strings on add_tactic_doc (#2201) …
Deleted tactic.interactive.normed_aView on Github →
2020-03-16 17:51
src/tactic/norm_num.lean
feat(tactic): command for adding tactic, command, and attribute documentation (#2114) …
Added tactic.interactive.normed_aView on Github →