Commit 2024-12-28 03:20 aa726920
View on Github →chore: use app_delab
(#20249)
This has the same behavior as delab app.
, but protects against typos.
The feature appeared in https://github.com/leanprover/lean4/pull/4976, though won't be documented until https://github.com/leanprover/lean4/pull/6450.