nonDep -> nondep

Author: kmill

src/Lean/Expr.lean

@@ -396,16 +396,16 @@ inductive Expr where
   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*).
+  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 kernel does not verify `nonDep` when type checking. This is an elaborator feature.
+  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)
+  | letE (declName : Name) (type : Expr) (value : Expr) (body : Expr) (nondep : Bool)
 
   /--
   Natural number and string literal values.
@@ -670,9 +670,9 @@ def mkSimpleThunkType (type : Expr) : Expr :=
 def mkSimpleThunk (type : Expr) : Expr :=
   mkLambda `_ BinderInfo.default (mkConst `Unit) type
 
-/-- 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 `let x : t := v; b`, a `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 :=
@@ -724,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) (nonDep : Bool) : Expr := mkLet n t v b nonDep
+@[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
@@ -875,7 +875,7 @@ def isLet : Expr → Bool
 
 /-- Return `true` if the given expression is a non-dependent let-expression (a have-expression). -/
 def isHave : Expr → Bool
-  | letE (nonDep := nonDep) .. => nonDep
+  | letE (nondep := nondep) .. => nondep
   | _       => false
 
 @[export lean_expr_is_have] def isHaveEx : Expr → Bool := isHave
@@ -1020,8 +1020,8 @@ def letBody! : Expr → Expr
   | letE _ _ _ b .. => b
   | _               => panic! "let expression expected"
 
-def letNonDep! : Expr → Bool
-  | letE _ _ _ _ nonDep => nonDep
+def letNondep! : Expr → Bool
+  | letE _ _ _ _ nondep => nondep
   | _                   => panic! "let expression expected"
 
 def consumeMData : Expr → Expr
@@ -1854,26 +1854,26 @@ 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) (newNonDep : Bool) : 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 && nonDep == newNonDep then
+  | letE n t v b nondep =>
+    if ptrEq t newType && ptrEq v newVal && ptrEq b newBody && nondep == newNondep then
       e
     else
-      letE n newType newVal newBody newNonDep
+      letE n newType newVal newBody newNondep
   | _              => panic! "let expression expected"
 
 @[implemented_by updateLet!Impl]
-def updateLet! (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) (newNonDep : Bool) : Expr :=
+def updateLet! (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) (newNondep : Bool) : Expr :=
   match e with
-  | letE n _ _ _ _ => letE n newType newVal newBody newNonDep
+  | letE n _ _ _ _ => letE n newType newVal newBody newNondep
   | _              => panic! "let expression expected"
 
-/-- Like `Expr.updateLet!` but preserves the `nonDep` flag. -/
+/-- 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
+  | 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

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1028,19 +1028,19 @@ def delabForall : Delab := do
 
 @[builtin_delab letE]
 def delabLetE : Delab := do
-  let Expr.letE n t v b nonDep ← 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
-    if nonDep then
+    if nondep then
       `(have $stxN : $stxT := $stxV; $stxB)
     else
       `(let $stxN : $stxT := $stxV; $stxB)
-  else if nonDep then
+  else if nondep then
     `(have $stxN := $stxV; $stxB)
   else
     `(let $stxN := $stxV; $stxB)
@@ -1301,14 +1301,14 @@ 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 nonDep ← 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 $
-        if nonDep then
+        if nondep then
           prependAndRec `(doElem|have $(mkIdent n) : $stxT := $stxV)
         else
           prependAndRec `(doElem|let $(mkIdent n) : $stxT := $stxV)

tests/lean/run/letNonDep.lean

@@ -1,8 +1,8 @@
 import Lean
 /-!
-# Tests of `Expr.letE (nonDep := true) ..`
+# Tests of `Expr.letE (nondep := true) ..`
 
-This file exercises the Lean/C++ interface to make sure that the `nonDep` field
+This file exercises the Lean/C++ interface to make sure that the `nondep` field
 is successfully part of the data model.
 -/
 
@@ -67,14 +67,14 @@ n : Nat
 
 /-!
 Testing `Expr.replace`, which is implemented in C++.
-The `nonDep` flag was previously cleared.
+The `nondep` flag was previously cleared.
 -/
 /-- info: Lean.Expr.letE `n (Lean.Expr.bvar 1) (Lean.Expr.bvar 1) (Lean.Expr.bvar 1) true -/
 #guard_msgs in #eval Expr.replace (fun e => if let .bvar i := e then some (.bvar (i + 1)) else none) (mkHave `n (.bvar 0) (.bvar 0) (.bvar 0))
 
 /-!
 Testing `instantiateMvars`, which is implemented in C++.
-The `nonDep` flag was previously cleared.
+The `nondep` flag was previously cleared.
 -/
 /--
 info: Lean.Expr.letE `n (Lean.Expr.const `Nat []) (Lean.Expr.const `Nat.zero []) (Lean.Expr.const `Unit []) true