mkLetFVars with nondependent let

Stream: lean4

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

When a let-binding is introduced via withLetDecl (nondep := true), abstracting it away later via mkLetFVars does not produce a have, but rather a lambda. It makes sense in terms of the implementation - nondependent bindings are stored as cdecls - but is certainly quite unintuitive. Should this be considered a bug or intended behavior?

import Lean

open Lean Meta Elab Term

#version -- Lean 4.23.0-nightly-2025-07-26

-- let x := True.intro; x
run_meta do
  let t ← withLetDecl `x (.const ``True []) (.const ``True.intro []) (nondep := False) fun x =>
    mkLetFVars #[x] x
  logInfo t

-- fun x => x
run_meta do
  let t ← withLetDecl `x (.const ``True []) (.const ``True.intro []) (nondep := True) fun x =>
    mkLetFVars #[x] x
  logInfo t

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Oh, and it works as expected with generalizeNondepLet := false:

-- have x := True.intro; x
run_meta do
  let t ← withLetDecl `x (.const ``True []) (.const ``True.intro []) (nondep := true) fun x =>
    mkLetFVars (generalizeNondepLet := false) #[x] x
  logInfo t

The documentation for it is buried far down, but it seems to be what I want here?

[Kyle Miller]

Yes, this is intended behavior. https://github.com/leanprover/lean4/blob/2be6c75c2baba5764a2dac57cabfcb69d273d4c9/src/Lean/LocalContext.lean#L63

If you are wanting to use withLetDecl and mkLetFVars in a pair like this, it's better to use mapLetDecl

[Kyle Miller]

There's some more documentation at docs#Lean.MetavarContext.MkBinding.mkBinding too

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Thanks! I can't use mapLetDecl because I am producing several Exprs whereas that only supports mapping one. I am basically inlining its implementation, though. The docstring on ldecl contains a mysterious remark:

Rule: never use (generalizeNondepLet := false) in mkBinding-family functions within a local context you do not own. See LocalDecl.setNondep for some additional discussion.

What does it mean to 'own' a local context?

[Kyle Miller]

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 said:

nondependent bindings are stored as cdecls

They're being stored as ldecls.

I linked to docstrings with some explanation, but the short version is that there's an "inside" and an "outside" to nondependent lets. From "inside" the value is opaque, but from "outside" you can see what the value is. It's unfortunately more complex than you'd hope...

The API is designed so that you can create a nondep let and call whatever you want (it will appear cdecl-like), and then you're able to abstract it as a have still.

[Kyle Miller]

"own" is supposed to mean "I extended this local context with my own bindings, and I will only abstract those bindings"

[Kyle Miller]

the point is that you shouldn't do mk*FVars with (generalizeNondepLet := false) with fvars that you don't know exactly where they came from.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Ah ok, maybe it would be clearer to say 'never use ... on a local context entry you did not create'? I can make a small doc PR. UPDATE: It's lean4#9570.