mathlib3
f98ffdef - feat(tactic/decl_mk_const): performance improvement for library_search (#967)

Commit
6 years ago
feat(tactic/decl_mk_const): performance improvement for library_search (#967) * feat(tactic/decl_mk_const): auxiliary tactic for library_search [WIP] * use decl_mk_const in library_search * use decl_mk_const * move into tactic/basic.lean
Author
Committer
Parents
Loading