Def delab_not_in

Modification history

2026-05-26 13:45
Mathlib/Util/Delaborators.lean
chore: rename delaborators to match naming convention (#39822) …
Deleted delab_not_inView on Github →
2024-12-28 03:20
Mathlib/Util/Delaborators.lean
chore: use `app_delab` (#20249) …
Modified delab_not_inView on Github →
2023-10-30 00:16
Mathlib/Util/Delaborators.lean
feat: more delaborators (#7964)
Added delab_not_inView on Github →