Sebastian Graf daddac1797 feat: support expected type annotation in doPatDecl (#12866) ...

This PR adds `optType` support to the `doPatDecl` parser, allowing
`let ⟨width, height⟩ : Nat × Nat ← action` in do-notation. Previously,
only
the less ergonomic `let ⟨width, height⟩ : Nat × Nat := ← action`
workaround
was available. The type annotation is propagated to the monadic action
as an
expected type, matching `doIdDecl`'s existing behavior.

Both the legacy and new (BuiltinDo) elaborators are updated.

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

2026-03-10 11:42:03 +00:00

..

bin

perf: separate meta and non-meta initializers (#12016)

2026-02-26 08:05:19 +00:00

cmake

chore: reformat all cmake files (#12218)

2026-01-28 18:23:08 +00:00

include/lean

feat: non exponential codegen for reset-reuse (#12665)

2026-02-26 09:35:45 +00:00

Init

feat: add cbv_simproc infrastructure for user-extensible cbv simplification procedures (#12597)

2026-03-10 10:59:13 +00:00

initialize

feat: zero cost BaseIO (#10625)

2025-10-22 10:55:12 +02:00

kernel

perf: fuse fvar substitution into instantiateMVars (#12233)

2026-03-09 17:05:21 +00:00

lake

feat: bundle leantar with Lean (#12822)

2026-03-09 20:10:59 +00:00

Lean

feat: support expected type annotation in doPatDecl (#12866)

2026-03-10 11:42:03 +00:00

LeanChecker

feat: add declaration name to leanchecker error messages (#12525)

2026-02-17 16:08:00 +00:00

library

perf: fuse fvar substitution into instantiateMVars (#12233)

2026-03-09 17:05:21 +00:00

runtime

feat: unify name demangling with single Lean implementation (#12539)

2026-03-06 12:29:35 +00:00

shell

chore: move test suite setup to tests/CMakeLists.txt (#12278)

2026-02-03 13:22:20 +00:00

Std

feat: use unicode(...) in Init/Notation and elsewhere (#10384)

2026-03-09 22:17:32 +00:00

util

chore: update to c++20 (#12117)

2026-02-11 01:17:40 +00:00

cadical.mk

fix: cadical distribution on Linux (#8201)

2025-05-02 18:25:16 +00:00

CMakeLists.txt

feat: bundle leantar with Lean (#12822)

2026-03-09 20:10:59 +00:00

config.h.in

perf: use mimalloc by default (#7710)

2025-03-30 22:40:41 +00:00

githash.h.in

…

Init.lean

feat: add cbv_simproc infrastructure for user-extensible cbv simplification procedures (#12597)

2026-03-10 10:59:13 +00:00

lakefile.toml.in

chore: turn on new do elaborator in Core (#12656)

2026-03-09 12:38:33 +00:00

lean-toolchain

chore: relative lean-toolchains (#12652)

2026-02-25 10:23:35 +00:00

Lean.lean

refactor: move getOriginalConstKind? into its own module to avoid future import cycle (#12265)

2026-02-01 16:18:51 +00:00

lean.mk.in

chore: further split libleanshared on Windows to avoid symbol limit (#10136)

2025-08-26 16:01:57 +00:00

Leanc.lean

fix: Unicode path support for Lean Windows executables (#10133)

2025-08-27 11:28:55 +00:00

LeanChecker.lean

feat: re-integrate lean4checker as leanchecker (#11887)

2026-01-08 09:41:33 +00:00

out

feat: ac normalization in grind (#10146)

2025-08-27 03:28:30 +00:00

Std.lean

chore: more module system fixes and refinements for finishing batteries port (#10819)

2025-10-21 08:19:50 +00:00

stdlib_flags.h

chore: turn on new do elaborator in Core (#12656)

2026-03-09 12:38:33 +00:00

stdlib.make.in

chore: clean up stdlib.make.in (#12614)

2026-02-20 16:59:34 +00:00

version.h.in

feat: language reference links and examples in docstrings (#7240)

2025-03-12 09:17:27 +00:00