Def CategoryTheory.toAppExpr

Modification history

2024-09-12 19:09
Mathlib/Tactic/CategoryTheory/ToApp.lean
feat(Tactic/CategoryTheory/ToApp): Add `to_app` attribute (#16119) …
Added CategoryTheory.toAppExprView on Github →