Aesop

Stream: nightly-testing

[Kim Morrison]

@Jannis Limperg AesopTest/RulePattern.lean is failing on Aesop's nightly-testing branch. Would you be able to take a look at that?

[Jannis Limperg]

My initial suspicion is that some change to the delaborator causes non-roundtripping delaboration in the presence of coercions. I'll investigate further tomorrow.

[Jannis Limperg]

I've disabled script checks in this test until lean4#4315 is resolved.