Commit 2024-05-23 02:18 028c49cb
View on Github →feat(CategoryTheory): aesop_cat uses sorry if there is a sorry in the goal (#13110)
This makes it slightly more ergonomic to construct structures. While you're still working on the data you don't get bothered about the proofs (which hopefully will be done by aesop_cat anyway).