Changes to DiscrTree

Stream: std4

[Scott Morrison]

We have some changes coming to the implementation of DiscrTree. std4#316 is the Std bump for this; I'd appreciate some skeptical eyes on this one!

[Scott Morrison]

@Jannis Limperg, I've made Aesop compile again at https://github.com/leanprover-community/aesop/pull/79. If you could give it a skeptical look, and then make any changes you'd like, that would be great!

[Mario Carneiro]

Oh, are we getting rid of the simpleReduce flag? What's the rationale?

[Mario Carneiro]

the changes themselves seem fine

[Scott Morrison]

Instead of the simpleReduce flag, all the DiscrTree functions now take WhnfCoreConfig argument. simpleReduce := false is {}, and simpleReduce := true is (I think?) { iota := false, proj := .no }.

[Joachim Breitner]

If you merge https://github.com/leanprover/std4/pull/285 first, then more (but not all) of the refactoring is contained to std4, as it moves some operations on DiscrTrees scattered throughout mathlib and Aesop to std4. But maybe that's too distracting at this point, and I can update my PR afterwards as well, of course.

[Joachim Breitner]

Whatever is most easiest. Maybe std4#316 could just move the operations to std since it's already touching all the code.

[Scott Morrison]

I don't particularly mind the ordering these happen in, but I would prefer to keep the migration and update steps in separate PRs.

[Joachim Breitner]

Fair enough, then better just go ahead with your update, and I'll continue with the migration afterwards.

[Jannis Limperg]

@Scott Morrison Thanks for fixing up Aesop! I've reviewed the PR and made some trivial changes.