feat: lemmas about Std.Range (#6396)

This PR adds lemmas reducing for loops over `Std.Range` to for loops over `List.range'`. Equivalent theorems previously existed in Batteries, but the underlying definitions have changed so these are written from scratch.
leanprover · Dec 16, 2024 · 791bea0 · 791bea0
1 parent 5c2ef51
commit 791bea0
Show file tree

Hide file tree

Showing 13 changed files with 697 additions and 500 deletions.
diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
@@ -7,7 +7,7 @@ The integers, with addition, multiplication, and subtraction.
 -/
 prelude
 import Init.Data.Cast
-import Init.Data.Nat.Div
+import Init.Data.Nat.Div.Basic
 
 set_option linter.missingDocs true -- keep it documented
 open Nat

diff --git a/src/Init/Data/List/Notation.lean b/src/Init/Data/List/Notation.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import Init.Data.Nat.Div
+import Init.Data.Nat.Div.Basic
 
 /-!
 # Notation for `List` literals.

diff --git a/src/Init/Data/Nat.lean b/src/Init/Data/Nat.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Nat.Basic
-import Init.Data.Nat.Div
+import Init.Data.Nat.Div.Basic
 import Init.Data.Nat.Dvd
 import Init.Data.Nat.Gcd
 import Init.Data.Nat.MinMax

diff --git a/src/Init/Data/Nat/Bitwise/Basic.lean b/src/Init/Data/Nat/Bitwise/Basic.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Nat.Basic
-import Init.Data.Nat.Div
+import Init.Data.Nat.Div.Basic
 import Init.Coe
 
 namespace Nat