RFC: `let` notation inside declaration binders

[eric-wieser]

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 :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

[Kha]

The simplest workaround here should be to move the relevant part of the type to the RHS of :. This means the binders have to be reintroduced in the body, but for proofs that can be done with intros so I'd say it's really not too bad. This strategy also extends to open in etc.

[eric-wieser]

This strategy also extends to open in etc.

Does intros really replay open in / set_option _ in clauses in binders like it does let?

[Kha]

It doesn't, you're right about that part