leanprover · kim-em · Aug 26, 2026
@@ -81,8 +81,8 @@ private theorem oneExtendPrefixLength (b : Broadcast) :
   by_cases H : left.ndim <= right.ndim
   . simp_all [Shape.ndim]
   . simp_all [Shape.ndim]
-    aesop (config := { warnOnNonterminal := false })
-    rw [Nat.sub_add_cancel]
+    have hn : ¬ (left.val.length ≤ right.val.length) := by omega
+    simp only [hn, ↓reduceIte, List.length_append, List.length_replicate]
     omega
 
 private def matchPairs (b : Broadcast) : Option Shape :=

@@ -155,7 +155,7 @@ private def roundTripUInt32BE (x : UInt32) : Bool := (toBEByteArray x).toUInt32B
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (x : UInt32) : roundTripUInt32LE x && roundTripUInt32BE x := by plausible
@@ -183,6 +183,7 @@ theorem _root_.ByteArray.replicateSize (n : Nat) : (ByteArray.replicate n v).siz
   rw [ByteArray.replicateSizeAux]
   unfold ByteArray.emptyWithCapacity ByteArray.size
   simp
+  rfl
 
 def _root_.ByteArray.zeros (n : Nat) : ByteArray := ByteArray.replicate n 0
 
@@ -247,7 +248,7 @@ private local instance : SampleableExt ByteArray :=
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (arr : ByteArray) :
@@ -258,7 +259,7 @@ example (arr : ByteArray) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (arr : ByteArray) :

@@ -54,7 +54,7 @@ open Plausible
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (x y : Nat) :
@@ -71,7 +71,7 @@ local instance : SampleableExt (Nat × Nat) :=
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (xy : Nat × Nat) :

@@ -1373,7 +1373,7 @@ private def canCastLosslessIntRoundTrip (fromDtype : Dtype) (n : Int) (toDtype :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (fromDtype toDtype : Dtype) (n : Nat) :
@@ -1384,7 +1384,7 @@ example (fromDtype toDtype : Dtype) (n : Nat) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 -- One dtype should always go back and forth
@@ -1395,7 +1395,7 @@ example (dtype : Dtype) (n : Nat) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 -- Lossless translations should be OK
@@ -1411,7 +1411,7 @@ example (fromDtype toDtype : Dtype) (n : Nat) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (a b : UInt16) :
@@ -1424,7 +1424,7 @@ example (a b : UInt16) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (a : UInt16) :
@@ -1440,7 +1440,7 @@ example (a : UInt16) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (a b : UInt16) :
@@ -1452,7 +1452,7 @@ example (a b : UInt16) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (a b : UInt8) :
@@ -1464,7 +1464,7 @@ example (a b : UInt8) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (a b : UInt8) :
@@ -1478,7 +1478,7 @@ example (a b : UInt8) :
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
 example (a b : Dtype) : Dtype.join a b == Dtype.join b a := by plausible

@@ -679,7 +679,7 @@ section Test
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
   #guard_msgs in
   example (bits : UInt16) :
@@ -719,7 +719,7 @@ warning: declaration uses 'sorry'
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
   example (bits : UInt16) :
@@ -777,7 +777,7 @@ warning: declaration uses 'sorry'
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
   example (bits : UInt8) :
@@ -790,7 +790,7 @@ warning: declaration uses 'sorry'
 /--
 info: Unable to find a counter-example
 ---
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs in
   example (bits : UInt8) :

@@ -37,7 +37,7 @@ namespace Iterator
 set_option synthInstance.checkSynthOrder false
 
 instance forInInstance [Monad m] [inst : Iterator iter value] : ForIn m iter value where
-  forIn {α} [Monad m] (iter : iter) (x : α) (f : value -> α -> m (ForInStep α)) : m α := do
+  forIn {α} (iter : iter) (x : α) (f : value -> α -> m (ForInStep α)) : m α := do
     let mut iter := iter
     let mut res := x
     for _ in [0:inst.size iter] do

@@ -125,7 +125,7 @@ def fromNpyString (s : String) : Err Dtype :=
   if s.length == 0 then .error "Empty dtype string" else
   do
     let order <- ByteOrder.fromChar (s.get 0)
-    let nameStr := s.drop 1
+    let nameStr := (s.drop 1).toString
     -- bf16 stored as "<V2" by ml_dtypes/JAX/TensorFlow (littleEndian)
     -- We only recognize "<V2" as bf16 to avoid collision with "|V2" (actual void data).
     -- Only littleEndian V2 is bf16. Tensor.toNpy always writes LE so this is safe.

@@ -1,45 +1,46 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover/lean4-cli.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "41c5d0b8814dec559e2e1441171db434fe2281cc",
+   "rev": "6130a47896ce867c6a4a55373441e59e565bad0f",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.23.0",
+   "inputRev": "v4.33.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a22e7c1fa7707fb7ea75f2f9fd6b14de2b7b87a9",
+   "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.23.0",
+   "inputRev": "v4.33.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "247ff80701c76760523b5d7c180b27b7708faf38",
+   "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.23.0",
+   "inputRev": "v4.33.0",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "d117e2c28cba42e974bc22568ac999492a34e812",
+   "scope": "leanprover-community",
+   "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.23.0",
+   "inputRev": "v4.33.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "TensorLib",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
@@ -28,10 +28,10 @@ lean_exe "tensorlib" where
   root := `Main
 
 require aesop from git
-  "https://github.com/leanprover-community/aesop" @ "v4.23.0"
+  "https://github.com/leanprover-community/aesop" @ "v4.33.0"
 
 require plausible from git
-  "https://github.com/leanprover-community/plausible" @ "v4.23.0"
+  "https://github.com/leanprover-community/plausible" @ "v4.33.0"
 
 require Cli from git
-  "https://github.com/leanprover/lean4-cli.git" @ "v4.23.0"
+  "https://github.com/leanprover/lean4-cli.git" @ "v4.33.0"
@@ -1 +1 @@
-leanprover/lean4:v4.23.0
+leanprover/lean4:v4.33.1