chore: bump to nightly-2025-03-12 (#341)

Author: david-christiansen

Manual/BasicTypes.lean

@@ -241,6 +241,8 @@ end ShortCircuit
 
 {docstring cond}
 
+{docstring Bool.dcond}
+
 {docstring Bool.not}
 
 {docstring Bool.and}

Manual/BasicTypes/Array.lean

@@ -193,6 +193,10 @@ tag := "array-api"
 
 {docstring Array.appendList}
 
+{docstring Array.leftpad}
+
+{docstring Array.rightpad}
+
 ## Size
 
 {docstring Array.size}
@@ -274,6 +278,8 @@ tag := "array-api"
 
 {docstring Array.swapAt!}
 
+{docstring Array.replace}
+
 {docstring Array.set}
 
 {docstring Array.set!}

Manual/BasicTypes/Int.lean

@@ -95,7 +95,7 @@ end
 
 {docstring Int.toNat}
 
-{docstring Int.toNat'}
+{docstring Int.toNat?}
 
 {docstring Int.toISize}
 

Manual/BuildTools/Lake/Config.lean

@@ -672,7 +672,7 @@ package $name where
 $[$_:docComment]?
 $[@[$_,*]]?
 package $_:identOrStr {
-  $[$_:declField $[,]?]*
+  $[$_:declField];*
 }
 $[where
   $[$_:letRecDecl];*]?
@@ -767,7 +767,7 @@ lean_lib $_:identOrStr where
 $[$_:docComment]?
 $[$_:attributes]?
 lean_lib $_:identOrStr {
-  $[$_:declField $[,]?]*
+  $[$_:declField];*
 }
 $[where
   $[$_:letRecDecl];*]?
@@ -800,7 +800,7 @@ lean_exe $_:identOrStr where
 ```grammar
 $[$_:docComment]? $[$_:attributes]?
 lean_exe $_:identOrStr {
-  $[$_:declField $[,]?]*
+  $[$_:declField];*
 }
 $[where
   $[$_:letRecDecl];*]?

Manual/Tactics.lean

@@ -371,7 +371,7 @@ In this proof state, the universe level of `α` is unknown:
 ∀ (α : _) (x : α) (xs : List α), x ∈ xs → xs.length > 0 := by
   intros α x xs elem
 /--
-α : Type ?u.891
+α : Type ?u.896
 x : α
 xs : List α
 elem : x ∈ xs

Manual/Terms.lean

@@ -694,6 +694,9 @@ They are encoded using the {name}`optParam` and {name}`autoParam` {tech}[gadgets
 {docstring autoParam}
 
 ## Generalized Field Notation
+%%%
+tag := "generalized-field-notation"
+%%%
 
 The {ref "structure-fields"}[section on structure fields] describes the notation for projecting a field from a term whose type is a structure.
 Generalized field notation consists of a term followed by a dot (`.`) and an identifier, not separated by spaces.

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d8b9226cb22503302167548284c399dd163d5e4e",
+   "rev": "18253d526eb256effbf62f896994f5043024f15a",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-03-07
+leanprover/lean4:nightly-2025-03-12