RefinedDiscrTree

[JovanGerb]

This is the same as my DiscrTree PR in Std, but I've decided to move it over to Mathlib now. Additionally, I have added the rw?? tactic which uses this RefinedDiscrTree in combination with shift-clicking on the goal to do targeted library rewriting.

I've made a new version of Lean's DiscrTree called RefinedDiscrTree with a lot of new features. It is able to index lambda's, forall's, and their bound variables. It also gives library metavariables an index so that it can keep track of which metavariables are the same. It also gives a score to each match pattern, so that you can get the results in order of how relevant they are.

The file uses the StateListT monad transformer (which does not satisfy the associativity monad law) that I made, so I also added its definition in another file.

The main purpose is for use is to get better results in library searches, for tactics like exact? and apply?, and I want to publish a library rewrite tactic that uses this discrimination tree.

---