feat: add the nondep field of Expr.letE to the C++ data model

src/Lean/Compiler/LCNF/Level.lean

@@ -67,7 +67,7 @@ partial def normExpr (e : Expr) : M Expr := do
     | .const _ us      => return e.updateConst! (← us.mapM normLevel)
     | .sort u          => return e.updateSort! (← normLevel u)
     | .app f a         => return e.updateApp! (← normExpr f) (← normExpr a)
-    | .letE _ t v b _  => return e.updateLet! (← normExpr t) (← normExpr v) (← normExpr b)
+    | .letE _ t v b _  => return e.updateLetE! (← normExpr t) (← normExpr v) (← normExpr b)
     | .forallE _ d b _ => return e.updateForallE! (← normExpr d) (← normExpr b)
     | .lam _ d b _     => return e.updateLambdaE! (← normExpr d) (← normExpr b)
     | .mdata _ b       => return e.updateMData! (← normExpr b)

src/Lean/Elab/PreDefinition/WF/Preprocess.lean

@@ -117,7 +117,7 @@ builtin_dsimproc paramLet (_) := fun e => do
   let u ← getLevel e.letType!
   let body' := e.letBody!.instantiate1 <|
     mkApp2 (.const ``wfParam [u]) e.letType! (.bvar 0)
-  return .continue <| e.updateLet! e.letType! v body'
+  return .continue <| e.updateLetE! e.letType! v body'
 
 def preprocess (e : Expr) : MetaM Simp.Result := do
   unless wf.preprocess.get (← getOptions) do

src/Lean/Expr.lean

@@ -391,20 +391,19 @@ inductive Expr where
   /--
   Let-expressions.
 
-  **IMPORTANT**: The `nonDep` flag is for "local" use only. That is, a module should not "trust" its value for any purpose.
-  In the intended use-case, the compiler will set this flag, and be responsible for maintaining it.
-  Other modules may not preserve its value while applying transformations.
+  The let-expression `let x : Nat := 2; Nat.succ x` is represented as
+  ```
+  Expr.letE `x (.const `Nat []) (.lit (.natVal 2)) (.app (.const `Nat.succ []) (.bvar 0)) true
+  ```
 
+  If the `nonDep` flag is `true`, then the elaborator treats this as a *non-dependent `let`* (known as a *`have` expression*).
   Given an environment, a metavariable context, and a local context,
   we say a let-expression `let x : t := v; e` is non-dependent when it is equivalent
   to `(fun x : t => e) v`. In contrast, the dependent let-expression
   `let n : Nat := 2; fun (a : Array Nat n) (b : Array Nat 2) => a = b` is type correct,
   but `(fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2` is not.
 
-  The let-expression `let x : Nat := 2; Nat.succ x` is represented as
-  ```
-  Expr.letE `x (.const `Nat []) (.lit (.natVal 2)) (.app (.const `Nat.succ []) (.bvar 0)) true
-  ```
+  The kernel does not verify `nonDep` when type checking. This is an elaborator feature.
   -/
   | letE (declName : Name) (type : Expr) (value : Expr) (body : Expr) (nonDep : Bool)
 
@@ -671,12 +670,14 @@ def mkSimpleThunkType (type : Expr) : Expr :=
 def mkSimpleThunk (type : Expr) : Expr :=
   mkLambda `_ BinderInfo.default (mkConst `Unit) type
 
-/--
-`.letE x t v b nonDep` is now the preferred form.
--/
-def mkLet (x : Name) (t : Expr) (v : Expr) (b : Expr) (nonDep : Bool := false) : Expr :=
+/-- Returns `let x : t := v; b`, a dependent `let` expression. If `nonDep := true`, then returns a `have`. -/
+@[inline] def mkLet (x : Name) (t : Expr) (v : Expr) (b : Expr) (nonDep : Bool := false) : Expr :=
   .letE x t v b nonDep
 
+/-- Returns `have x : t := v; b`, a non-dependent `let` expression. -/
+@[inline] def mkHave (x : Name) (t : Expr) (v : Expr) (b : Expr) : Expr :=
+  .letE x t v b true
+
 @[match_pattern] def mkAppB (f a b : Expr) := mkApp (mkApp f a) b
 @[match_pattern] def mkApp2 (f a b : Expr) := mkAppB f a b
 @[match_pattern] def mkApp3 (f a b c : Expr) := mkApp (mkAppB f a b) c
@@ -723,7 +724,7 @@ def mkStrLit (s : String) : Expr :=
 @[export lean_expr_mk_app] def mkAppEx : Expr → Expr → Expr := mkApp
 @[export lean_expr_mk_lambda] def mkLambdaEx (n : Name) (d b : Expr) (bi : BinderInfo) : Expr := mkLambda n bi d b
 @[export lean_expr_mk_forall] def mkForallEx (n : Name) (d b : Expr) (bi : BinderInfo) : Expr := mkForall n bi d b
-@[export lean_expr_mk_let] def mkLetEx (n : Name) (t v b : Expr) : Expr := mkLet n t v b
+@[export lean_expr_mk_let] def mkLetEx (n : Name) (t v b : Expr) (nonDep : Bool) : Expr := mkLet n t v b nonDep
 @[export lean_expr_mk_lit] def mkLitEx : Literal → Expr := mkLit
 @[export lean_expr_mk_mdata] def mkMDataEx : MData → Expr → Expr := mkMData
 @[export lean_expr_mk_proj] def mkProjEx : Name → Nat → Expr → Expr := mkProj
@@ -867,11 +868,18 @@ def isBinding : Expr → Bool
   | forallE .. => true
   | _          => false
 
-/-- Return `true` if the given expression is a let-expression. -/
+/-- Return `true` if the given expression is a let-expression or a have-expression. -/
 def isLet : Expr → Bool
   | letE .. => true
   | _       => false
 
+/-- Return `true` if the given expression is a non-dependent let-expression (a have-expression). -/
+def isHave : Expr → Bool
+  | letE (nonDep := nonDep) .. => nonDep
+  | _       => false
+
+@[export lean_expr_isHave] def isHaveEx : Expr → Bool := isHave
+
 /-- Return `true` if the given expression is a metadata. -/
 def isMData : Expr → Bool
   | mdata .. => true
@@ -1012,6 +1020,10 @@ def letBody! : Expr → Expr
   | letE _ _ _ b .. => b
   | _               => panic! "let expression expected"
 
+def letNonDep! : Expr → Bool
+  | letE _ _ _ _ nonDep => nonDep
+  | _                   => panic! "let expression expected"
+
 def consumeMData : Expr → Expr
   | mdata _ e => consumeMData e
   | e         => e
@@ -1842,21 +1854,28 @@ def updateLambda! (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody
   | lam n d b bi => updateLambda! (lam n d b bi) bi newDomain newBody
   | _            => panic! "lambda expected"
 
-@[inline] private unsafe def updateLet!Impl (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) : Expr :=
+@[inline] private unsafe def updateLet!Impl (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) (newNonDep : Bool) : Expr :=
   match e with
   | letE n t v b nonDep =>
-    if ptrEq t newType && ptrEq v newVal && ptrEq b newBody then
+    if ptrEq t newType && ptrEq v newVal && ptrEq b newBody && nonDep == newNonDep then
       e
     else
-      letE n newType newVal newBody nonDep
+      letE n newType newVal newBody newNonDep
   | _              => panic! "let expression expected"
 
 @[implemented_by updateLet!Impl]
-def updateLet! (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) : Expr :=
+def updateLet! (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) (newNonDep : Bool) : Expr :=
   match e with
-  | letE n _ _ _ c => letE n newType newVal newBody c
+  | letE n _ _ _ _ => letE n newType newVal newBody newNonDep
   | _              => panic! "let expression expected"
 
+/-- Like `Expr.updateLet!` but preserves the `nonDep` flag. -/
+@[inline]
+def updateLetE! (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) : Expr :=
+  match e with
+  | letE n t v b nonDep => updateLet! (letE n t v b nonDep) newType newVal newBody nonDep
+  | _                   => panic! "let expression expected"
+
 def updateFn : Expr → Expr → Expr
   | e@(app f a), g => e.updateApp! (updateFn f g) a
   | _,           g => g
@@ -1965,7 +1984,7 @@ def letFun? (e : Expr) : Option (Name × Expr × Expr × Expr) :=
   | .app (.app (.app (.app (.const ``letFun _) t) _β) v) f =>
     match f with
     | .lam n _ b _ => some (n, t, v, b)
-    | _ => some (.anonymous, t, v, .app f (.bvar 0))
+    | _ => some (.anonymous, t, v, .app (f.liftLooseBVars 0 1) (.bvar 0))
   | _ => none
 
 /--
@@ -1982,15 +2001,15 @@ def letFunAppArgs? (e : Expr) : Option (Array Expr × Name × Expr × Expr × Ex
   let rest := args.extract 4 args.size
   match f with
   | .lam n _ b _ => some (rest, n, t, v, b)
-  | _ => some (rest, .anonymous, t, v, .app f (.bvar 0))
+  | _ => some (rest, .anonymous, t, v, .app (f.liftLooseBVars 0 1) (.bvar 0))
 
 /-- Maps `f` on each immediate child of the given expression. -/
 @[specialize]
 def traverseChildren [Applicative M] (f : Expr → M Expr) : Expr → M Expr
   | e@(forallE _ d b _) => pure e.updateForallE! <*> f d <*> f b
   | e@(lam _ d b _)     => pure e.updateLambdaE! <*> f d <*> f b
   | e@(mdata _ b)       => e.updateMData! <$> f b
-  | e@(letE _ t v b _)  => pure e.updateLet! <*> f t <*> f v <*> f b
+  | e@(letE _ t v b _)  => pure e.updateLetE! <*> f t <*> f v <*> f b
   | e@(app l r)         => pure e.updateApp! <*> f l <*> f r
   | e@(proj _ _ b)      => e.updateProj! <$> f b
   | e                   => pure e

src/Lean/Meta/AbstractMVars.lean

@@ -78,7 +78,7 @@ partial def abstractExprMVars (e : Expr) : M Expr := do
     | e@(Expr.mdata _ b)       => return e.updateMData! (← abstractExprMVars b)
     | e@(Expr.lam _ d b _)     => return e.updateLambdaE! (← abstractExprMVars d) (← abstractExprMVars b)
     | e@(Expr.forallE _ d b _) => return e.updateForallE! (← abstractExprMVars d) (← abstractExprMVars b)
-    | e@(Expr.letE _ t v b _)  => return e.updateLet! (← abstractExprMVars t) (← abstractExprMVars v) (← abstractExprMVars b)
+    | e@(Expr.letE _ t v b _)  => return e.updateLetE! (← abstractExprMVars t) (← abstractExprMVars v) (← abstractExprMVars b)
     | e@(Expr.mvar mvarId)     =>
       let decl := (← getMCtx).getDecl mvarId
       if decl.depth != (← getMCtx).depth then

src/Lean/Meta/Closure.lean

@@ -193,7 +193,7 @@ partial def collectExprAux (e : Expr) : ClosureM Expr := do
   | Expr.proj _ _ s      => return e.updateProj! (← collect s)
   | Expr.forallE _ d b _ => return e.updateForallE! (← collect d) (← collect b)
   | Expr.lam _ d b _     => return e.updateLambdaE! (← collect d) (← collect b)
-  | Expr.letE _ t v b _  => return e.updateLet! (← collect t) (← collect v) (← collect b)
+  | Expr.letE _ t v b _  => return e.updateLetE! (← collect t) (← collect v) (← collect b)
   | Expr.app f a         => return e.updateApp! (← collect f) (← collect a)
   | Expr.mdata _ b       => return e.updateMData! (← collect b)
   | Expr.sort u          => return e.updateSort! (← collectLevel u)

src/Lean/Meta/ExprDefEq.lean

@@ -851,7 +851,7 @@ mutual
       | .proj _ _ s      => return e.updateProj! (← check s)
       | .lam _ d b _     => return e.updateLambdaE! (← check d) (← check b)
       | .forallE _ d b _ => return e.updateForallE! (← check d) (← check b)
-      | .letE _ t v b _  => return e.updateLet! (← check t) (← check v) (← check b)
+      | .letE _ t v b _  => return e.updateLetE! (← check t) (← check v) (← check b)
       | .bvar ..         => return e
       | .sort ..         => return e
       | .const ..        => return e

src/Lean/Meta/ExprLens.lean

@@ -36,8 +36,8 @@ private def lensCoord (g : Expr → M Expr) (n : Nat) (e : Expr) : M Expr := do
   | 1, .lam n y b c     => withLocalDecl n c y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x]
   | 0, .forallE _ y b _ => return e.updateForallE! (← g y) b
   | 1, .forallE n y b c => withLocalDecl n c y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x]
-  | 0, .letE _ y a b _  => return e.updateLet! (← g y) a b
-  | 1, .letE _ y a b _  => return e.updateLet! y (← g a) b
+  | 0, .letE _ y a b _  => return e.updateLetE! (← g y) a b
+  | 1, .letE _ y a b _  => return e.updateLetE! y (← g a) b
   | 2, .letE n y a b _  => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x]
   | 0, .proj _ _ b      => e.updateProj! <$> g b
   | n, .mdata _ a       => e.updateMData! <$> lensCoord g n a

src/Lean/Meta/InferType.lean

@@ -38,7 +38,7 @@ where
       match e with
       | .forallE _ d b _ => return e.updateForallE! (← visit d offset) (← visit b (offset+1))
       | .lam _ d b _     => return e.updateLambdaE! (← visit d offset) (← visit b (offset+1))
-      | .letE _ t v b _  => return e.updateLet! (← visit t offset) (← visit v offset) (← visit b (offset+1))
+      | .letE _ t v b _  => return e.updateLetE! (← visit t offset) (← visit v offset) (← visit b (offset+1))
       | .mdata _ b       => return e.updateMData! (← visit b offset)
       | .proj _ _ b      => return e.updateProj! (← visit b offset)
       | .app .. =>

src/Lean/Meta/KAbstract.lean

@@ -36,7 +36,7 @@ def kabstract (e : Expr) (p : Expr) (occs : Occurrences := .all) : MetaM Expr :=
         | .app f a         => return e.updateApp! (← visit f offset) (← visit a offset)
         | .mdata _ b       => return e.updateMData! (← visit b offset)
         | .proj _ _ b      => return e.updateProj! (← visit b offset)
-        | .letE _ t v b _  => return e.updateLet! (← visit t offset) (← visit v offset) (← visit b (offset+1))
+        | .letE _ t v b _  => return e.updateLetE! (← visit t offset) (← visit v offset) (← visit b (offset+1))
         | .lam _ d b _     => return e.updateLambdaE! (← visit d offset) (← visit b (offset+1))
         | .forallE _ d b _ => return e.updateForallE! (← visit d offset) (← visit b (offset+1))
         | e                => return e

src/Lean/Meta/SynthInstance.lean

@@ -135,7 +135,7 @@ partial def normExpr (e : Expr) : M Expr := do
     | .const _ us      => return e.updateConst! (← us.mapM normLevel)
     | .sort u          => return e.updateSort! (← normLevel u)
     | .app f a         => return e.updateApp! (← normExpr f) (← normExpr a)
-    | .letE _ t v b _  => return e.updateLet! (← normExpr t) (← normExpr v) (← normExpr b)
+    | .letE _ t v b _  => return e.updateLetE! (← normExpr t) (← normExpr v) (← normExpr b)
     | .forallE _ d b _ => return e.updateForallE! (← normExpr d) (← normExpr b)
     | .lam _ d b _     => return e.updateLambdaE! (← normExpr d) (← normExpr b)
     | .mdata _ b       => return e.updateMData! (← normExpr b)

src/Lean/Meta/Tactic/Lets.lean

@@ -227,7 +227,7 @@ partial def extractCore (fvars : List Expr) (e : Expr) (topLevel : Bool := false
       match e with
       | .bvar .. | .fvar .. | .mvar .. | .sort .. | .const .. | .lit .. => unreachable!
       | .mdata _ e'      => return e.updateMData! (← extractCore fvars e' (topLevel := topLevel))
-      | .letE n t v b _  => extractLetLike true n t v b (fun t v b => pure <| e.updateLet! t v b) (topLevel := topLevel)
+      | .letE n t v b _  => extractLetLike true n t v b (fun t v b => pure <| e.updateLetE! t v b) (topLevel := topLevel)
       | .app ..          =>
         if e.isLetFun then
           extractLetFun e (topLevel := topLevel)

src/Lean/Meta/Transform.lean

@@ -59,7 +59,7 @@ partial def transform {m} [Monad m] [MonadLiftT CoreM m] [MonadControlT CoreM m]
         match e with
         | .forallE _ d b _ => visitPost (e.updateForallE! (← visit d) (← visit b))
         | .lam _ d b _     => visitPost (e.updateLambdaE! (← visit d) (← visit b))
-        | .letE _ t v b _  => visitPost (e.updateLet! (← visit t) (← visit v) (← visit b))
+        | .letE _ t v b _  => visitPost (e.updateLetE! (← visit t) (← visit v) (← visit b))
         | .app ..          => e.withApp fun f args => do visitPost (mkAppN (← visit f) (← args.mapM visit))
         | .mdata _ b       => visitPost (e.updateMData! (← visit b))
         | .proj _ _ b      => visitPost (e.updateProj! (← visit b))

src/Lean/MetavarContext.lean

@@ -1052,7 +1052,7 @@ mutual
     | .proj _ _ s      => return e.updateProj! (← visit xs s)
     | .forallE _ d b _ => return e.updateForallE! (← visit xs d) (← visit xs b)
     | .lam _ d b _     => return e.updateLambdaE! (← visit xs d) (← visit xs b)
-    | .letE _ t v b _  => return e.updateLet! (← visit xs t) (← visit xs v) (← visit xs b)
+    | .letE _ t v b _  => return e.updateLetE! (← visit xs t) (← visit xs v) (← visit xs b)
     | .mdata _ b       => return e.updateMData! (← visit xs b)
     | .app ..          => e.withApp fun f args => elimApp xs f args
     | .mvar _          => elimApp xs e #[]
@@ -1385,7 +1385,7 @@ partial def main (e : Expr) : M Expr :=
       | .proj _ _ s      => return e.updateProj! (← main s)
       | .forallE _ d b _ => return e.updateForallE! (← main d) (← main b)
       | .lam _ d b _     => return e.updateLambdaE! (← main d) (← main b)
-      | .letE _ t v b _  => return e.updateLet! (← main t) (← main v) (← main b)
+      | .letE _ t v b _  => return e.updateLetE! (← main t) (← main v) (← main b)
       | .app ..          => e.withApp fun f args => visitApp f args
       | .mdata _ b       => return e.updateMData! (← main b)
       | .const _ us      => return e.updateConst! (← us.mapM visitLevel)

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1028,16 +1028,22 @@ def delabForall : Delab := do
 
 @[builtin_delab letE]
 def delabLetE : Delab := do
-  let Expr.letE n t v b _ ← getExpr | unreachable!
+  let Expr.letE n t v b nonDep ← getExpr | unreachable!
   let n ← getUnusedName n b
   let stxV ← descend v 1 delab
   let (stxN, stxB) ← withLetDecl n t v fun fvar => do
     let b := b.instantiate1 fvar
     return (← mkAnnotatedIdent n fvar, ← descend b 2 delab)
   if ← getPPOption getPPLetVarTypes <||> getPPOption getPPAnalysisLetVarType then
     let stxT ← descend t 0 delab
-    `(let $stxN : $stxT := $stxV; $stxB)
-  else `(let $stxN := $stxV; $stxB)
+    if nonDep then
+      `(have $stxN : $stxT := $stxV; $stxB)
+    else
+      `(let $stxN : $stxT := $stxV; $stxB)
+  else if nonDep then
+    `(have $stxN := $stxV; $stxB)
+  else
+    `(let $stxN := $stxV; $stxB)
 
 @[builtin_delab app.Char.ofNat]
 def delabChar : Delab := do
@@ -1295,14 +1301,17 @@ partial def delabDoElems : DelabM (List Syntax) := do
             prependAndRec `(doElem|let _ ← $ma:term)
       | _ => failure
   else if e.isLet then
-    let Expr.letE n t v b _ ← getExpr | unreachable!
+    let Expr.letE n t v b nonDep ← getExpr | unreachable!
     let n ← getUnusedName n b
     let stxT ← descend t 0 delab
     let stxV ← descend v 1 delab
     withLetDecl n t v fun fvar =>
       let b := b.instantiate1 fvar
       descend b 2 $
-        prependAndRec `(doElem|let $(mkIdent n) : $stxT := $stxV)
+        if nonDep then
+          prependAndRec `(doElem|have $(mkIdent n) : $stxT := $stxV)
+        else
+          prependAndRec `(doElem|let $(mkIdent n) : $stxT := $stxV)
   else if e.isLetFun then
     -- letFun.{u, v} : {α : Sort u} → {β : α → Sort v} → (v : α) → ((x : α) → β x) → β v
     let stxT ← withNaryArg 0 delab

src/Lean/Util/ReplaceExpr.lean

@@ -23,7 +23,7 @@ def replaceNoCache (f? : Expr → Option Expr) (e : Expr) : Expr :=
     | .forallE _ d b _ => let d := replaceNoCache f? d; let b := replaceNoCache f? b; e.updateForallE! d b
     | .lam _ d b _     => let d := replaceNoCache f? d; let b := replaceNoCache f? b; e.updateLambdaE! d b
     | .mdata _ b       => let b := replaceNoCache f? b; e.updateMData! b
-    | .letE _ t v b _  => let t := replaceNoCache f? t; let v := replaceNoCache f? v; let b := replaceNoCache f? b; e.updateLet! t v b
+    | .letE _ t v b _  => let t := replaceNoCache f? t; let v := replaceNoCache f? v; let b := replaceNoCache f? b; e.updateLetE! t v b
     | .app f a         => let f := replaceNoCache f? f; let a := replaceNoCache f? a; e.updateApp! f a
     | .proj _ _ b      => let b := replaceNoCache f? b; e.updateProj! b
     | e                => e