Changelog

leanprover/lean4 · · 7 commits

Do elaborator gets indexed monads; string compare speeds up

Lean4’s do-notation now handles indexed monads, while string comparison gets a faster C++ backend and path/string cleanups continue.

sgraf812 TwoFX hargoniX

Do notation now supports indexed monads (sgraf81265b3453)

DoOps gained splitMonadApp? and mkMonadApp, letting elabDoWith decompose and rebuild monad applications that carry instance arguments, such as indexed monads like Measure α. This removes a hard-coded m α assumption and makes custom do-elaboration work with a broader class of monads.

String comparison is now backed by a dedicated runtime primitive (hargoniXa3fff15)

String.compare was given an extern binding to a new C++ lean_string_compare implementation, so ordering can be computed directly instead of via the generic compareOfLessAndEq path. That should reduce comparison overhead for any code that orders strings.

Other misc changes

  • Do elaborator refactor: rename mkMonadicType to mkMonadApp across builtin do support and related call sites (sgraf812da8bcf7)
  • String-processing cleanup across compiler/docs/repr code, removing more String.length uses (TwoFXada1696)
  • More string/path refactors for FilePath and String utilities, including ASCII-length assumptions and slice-based path handling (TwoFXfa23847)
  • Stage0 rebuilt to pick up the runtime/stdlib changes (34df732)
  • Prep work for the String.compare optimization in runtime and headers (hargoniX8398048)