lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard
verified publisher icon leanprover

fix: improve proof search in IndPredBelow

Open nomeata opened this issue 1 year ago • 2 comments

MVarId.apply is clever in the order it returns mvars, by putting those arising from non-dependent arguments first. If we lean on that behavior, this fixes #1672.

H'T to @DanielFabian, this was found together in a call.

Also improves tracing.

nomeata avatar Jul 26 '24 09:07 nomeata