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.

Estimated changes