fun_prop and #6053

Stream: mathlib4

[Kim Morrison]

@Tomas Skrivan (and anyone else interested in helping out!) fun_prop is going to need some significant modifications to adapt to lean#6053. I'm running out of time tonight, but if you're able to take a look at this sometime, please feel free to push changes to lean-pr-testing-6053 directly.

Rather than passing around WhnfCoreConfig data, everything now reads these directly from the Meta.Config (via ← getConfig).

[Kim Morrison]

I'm eager to get this sorted soon as it is blocking Leo, so I'll be looking at this tomorrow if no one has beaten me to it. :-)

[Tomas Skrivan]

I will look into it tomorrow

[Kim Morrison]

I think I've got this sorted out now.

@Tomas Skrivan, if you wouldn't mind reviewing the commit https://github.com/leanprover-community/mathlib4/commit/7faa75a037bc3e518e9ff1aa8485be3154244806 on the lean-pr-testing-6053 branch, and letting me know if you see anything problematic, that would be very helpful.

[Tomas Skrivan]

Looks good! I just did a minor refactor to clean it up.

[Kim Morrison]

@Tomas Skrivan, thanks! We've already merged lean-pr-testing-6053 into nightly-testing, so I'll just cherry-pick your commit across now.