Commit 2021-10-13 09:00 467b715e

feat: librarySearch (#65) This adds a simple version of the librarySearch tactic from mathlib.

• The implementation uses discrimination trees, with the hope of better scalability.
• A new cache data structure is introduced to simplify the caching of such indexing data structures. Some todos:
• There is no "try this" yet. I'm waiting for code actions to land in Lean 4.
• It only does reducible matching for now. I hope that I'll be able to abuse the discrimination trees to do indexing for semireducible matching as well.
• Iff.mp, etc. projections are not implemented yet.