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.