aesop crash

Stream: general

[Kim Morrison]

@Jannis Limperg, you might be interested in looking into the stack overflow that results from inserting aesop after the intro in the proof of docs#compactumToCompHaus.faithful

[Kim Morrison]

While we're on the subject of aesop problems, the map_comp field of docs#Profinite.fintypeDiagram is currently proved by ext; aesop_cat, but just by aesop_cat fails. How can that be?

[Robert Maxton]

Kim Morrison said:

While we're on the subject of aesop problems, the map_comp field of docs#Profinite.fintypeDiagram is currently proved by ext; aesop_cat, but just by aesop_cat fails. How can that be?

I'd like to know this as well; it seems like aesop_cat no longer calls ext (and now that I think to go check, I indeed don't see the old ext shim anywhere). Instead it tries a little harder to use intros, but that only really works if the thing you're using ext with is a function-like thing, rather than, say, a sigma-like thing.

[Calle Sönne]

I am also interested in this, as I seem to be running into a similar issue on a branch of mine, where aesop_cat is unable to use ext (and is unable to prove something that ext <;> simp can prove).

In my situation I have made a custom ext-lemma using eqToHom, instead of dealing with HEq issues. I guess if aesop_cat doesn't call ext directly, then there is no way for it to use my custom lemma.