Def Lean.Meta.DiscrTree.insertIfSpecific

Modification history

2023-11-02 13:03
Mathlib/Lean/Meta/DiscrTree.lean
chore: bump Std to Std#254 (#8106)
Deleted Lean.Meta.DiscrTree.insertIfSpecificView on Github →
2023-10-31 09:38
Mathlib/Lean/Meta/DiscrTree.lean
chore: bump toolchain to v4.3.0-rc1 (#8051) …
Modified Lean.Meta.DiscrTree.insertIfSpecificView on Github →
2023-05-07 09:18
Mathlib/Lean/Meta/DiscrTree.lean
feat: library_search tries most specific lemmas first, and then those with shorter names first (#3725) …
Modified Lean.Meta.DiscrTree.insertIfSpecificView on Github →
2023-04-18 12:01
Mathlib/Lean/Meta/DiscrTree.lean
feat: `propose`, a forwards-reasoning analogue of `library_search`. (#2898) …
Modified Lean.Meta.DiscrTree.insertIfSpecificView on Github →
2023-03-15 00:24
Mathlib/Tactic/LibrarySearch.lean
feat: speed up library_search by discarding lemma with non-specific discrimination keys. (#2888) …
Added Lean.Meta.DiscrTree.insertIfSpecificView on Github →