search

leanprover-community / aesop

White-box automation for Lean 4
Apache License 2.0
155 stars 25 forks source link

chore: update for renamed fields in Subarray #122

Closed david-christiansen closed 2 months ago

david-christiansen commented 2 months ago

Adaptation for https://github.com/leanprover/lean4/pull/3851 and https://github.com/leanprover/std4/pull/733

david-christiansen commented 2 months ago

@JLimperg I'm not entirely sure what the failing test for lists is testing - can you see if it is the test or the implementation that needs to be updated?

JLimperg commented 2 months ago

I've fixed some of the tests. The others are fixed in #117; please merge the relevant parts of that PR.

david-christiansen commented 2 months ago

It looks like this was superseded by #123 - thanks for the help!

kmill commented 2 months ago

Sorry, I should have looked at the open PRs! I'd made the fix locally when getting mathlib back up to date.