RFC: `let` notation inside declaration binders

Proposal

Currently, Lean provides

def foo (x y : Nat) : Nat := x + y

as notation for

def foo : ∀ x y : Nat, Nat := fun x y => x + y

This RFC suggests extending this with

def bar (x : Nat) (let y : Nat := 2) : Nat := x + y

as notation for

def bar : ∀ x : Nat, let y : Nat := 2; Nat := fun x => let y : Nat := 2; x + y

Rocq already has this notation, as (y := 2). This notation is already claimed by optParams in Lean, but (let y := 2) seems like a natural alternative.

Motivation:

• Accidental use of optParams is a common trap (https://github.com/trishullab/PutnamBench/issues/166); the let syntax could be referenced in the docstring of optParam to help resolve confusion
• Allowing theorem signatures to represent letE in addition to forallE means that they can now completely capture any intermediate goal state in a proof, allowing mathlib's extract_goal to more faithfully extract the current goal with an identical local context at the start of the proof.

Optional extensions that this RFC is neutral on:

• Allow let binders as fun x (let y := 2 * x) (z : Fin y) => z.val
• Allow let binders as have foo (x : Nat) (let y : Nat := 2) :=
• Allow let binders in Exists and other custom binder types
• def foo (x : Nat) (open scoped Nat) (y : Fin (x)!) and similar for set_option

Community Feedback

• older Zulip discussion

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start with the proposal's let binder examples and review the linked older Zulip discussion. The issue names no implementation entry point or tests, and the optional extensions leave the scope open; done would require an agreed design and corresponding compiler support.