Def CategoryTheory.evalSorryIfSorry

Modification history

2024-05-23 02:18
Mathlib/CategoryTheory/Category/Basic.lean
feat(CategoryTheory): aesop_cat uses sorry if there is a sorry in the goal (#13110) …
Added CategoryTheory.evalSorryIfSorryView on Github →