lean4

test: cover `try`/`catch` coercion difference in new `do` elaborator (#13849)

feat: include error message in `instances`-level type-check failure (#13793)

fix: benchmark failure (#13848)

feat: verifiable `whileM` via ordered fixpoints for stronger specs (#13689)

feat: restrict `simpa using h` close to reducible transparency (#13636)