Joe Hendrix

I don't think either of these should be simp rules. There is active work on integrating SAT solving into Lean, and in the ground case, I think it'd be useful...

I think this is an interesting structure, but there needs to be a quite high bar before we have two DiscrTree implementations in Lean and Std. That's twice the potential...

Why do you think the performance overhead is fine? Isn't DiscrTree used as a filter? Are there any performance benchmarks for `exact?`? I am looking into merging that in Std...

I think the profiler is a good tool to use for performance analysis. For benchmarks, I think it's context specific. Since we are talking about first using this in the...

Are there other projects using this? I think we are potentially better served more abstract than this in `Std`, but I'm not quite sure how this is used.

I haven't looked at this closely, but I think this may be too niche to include in std.

I took a look at this again and am requesting a review from @digama0 since I think he is most familiar with this code.

I'm open to other approaches then reviving these classes, but it did seem like a way to get the monoid properties I wanted for writing fold/sum lemmas. `IsSymmOp` isn't strictly...

The associativity and commutative ones don't have a good reason. Perhaps I should use the Lean core versions. The Identity classes use an out parameter for the identity/neutral element.

I'm looking into both changing the core axioms and/or moving/removing ac_rfl. If ac_rfl is removed from core, then technically the classes could live in Std. However, I think it's good...