feat: start work on iterators and ranges (#672)

Co-authored-by: Paul Reichert <[email protected]>

Author: david-christiansen

.github/workflows/ci.yml

@@ -222,7 +222,7 @@ jobs:
       - name: Run LinkChecker (local links only)
         if: github.event_name == 'push' || github.event_name == 'pull_request'
         run: |
-          linkchecker './_out/html-multi/'
+          linkchecker --config=.linkchecker/linkcheckerrc './_out/html-multi/'
 
       # This saved number is used by a workflow_run trigger. It
       # manages labels that indicate the status of the built HTML.

.linkchecker/linkcheckerrc

@@ -0,0 +1,2 @@
+[filtering]
+ignorewarnings=url-content-too-large,url-too-long

Manual.lean

@@ -20,6 +20,7 @@ import Manual.Simp
 import Manual.Grind
 import Manual.VCGen
 import Manual.BasicTypes
+import Manual.Iterators
 import Manual.BasicProps
 import Manual.NotationsMacros
 import Manual.IO
@@ -118,6 +119,7 @@ draft := true
 
 {docstring Dynamic.get?}
 
+{include 0 Manual.Iterators}
 
 # Standard Library
 %%%
@@ -345,6 +347,32 @@ Std.ExtHashSet
 Std.TreeMap
 Std.DTreeMap
 Std.TreeSet
+Std.Iterators
+Std.Iterators.Iter
+Std.Iterators.Iter.Equiv
+Std.Iterators.Iter.TerminationMeasures
+Std.Iterators.IterM
+Std.Iterators.IterM.Equiv
+Std.Iterators.IterM.TerminationMeasures
+Std.Iterators.Iterator
+Std.Iterators.IteratorAccess
+Std.Iterators.IteratorLoop
+Std.Iterators.IteratorLoopPartial
+Std.Iterators.Finite
+Std.Iterators.Productive
+Std.Iterators.PostconditionT
+Std.Iterators.HetT
+Std.PRange
+Std.PRange.UpwardEnumerable
+Std.Rco
+Std.Rcc
+Std.Rci
+Std.Roo
+Std.Roc
+Std.Roi
+Std.Rio
+Std.Ric
+Std.Rii
 ```
 
 ```exceptions
@@ -836,6 +864,17 @@ Prod.lex
 Prod.Lex
 ```
 
+```exceptions
+Std.Iterators.Iter.instForIn'
+Std.Iterators.Iter.step_filter
+Std.Iterators.Iter.val_step_filter
+```
+
+```exceptions
+Std.Iterators.IterM.instForIn'
+Std.Iterators.IterM.toListRev.go
+```
+
 ```exceptions
 
 Lean.Elab.Tactic.elabSetOption

Manual/BasicTypes.lean

@@ -25,6 +25,7 @@ import Manual.BasicTypes.List
 import Manual.BasicTypes.Maps
 import Manual.BasicTypes.Subtype
 import Manual.BasicTypes.Thunk
+import Manual.BasicTypes.Range
 
 open Manual.FFIDocType
 
@@ -319,6 +320,8 @@ Most comparisons on Booleans should be performed using the {inst}`DecidableEq Bo
 
 {include 0 Manual.BasicTypes.ByteArray}
 
+{include 0 Manual.BasicTypes.Range}
+
 {include 0 Manual.BasicTypes.Maps}
 
 {include 0 Manual.BasicTypes.Subtype}

Manual/BasicTypes/Array.lean

@@ -336,6 +336,14 @@ tag := "array-api"
 
 ## Iteration
 
+{docstring Array.iter}
+
+{docstring Array.iterFromIdx}
+
+{docstring Array.iterM}
+
+{docstring Array.iterFromIdxM}
+
 {docstring Array.foldr}
 
 {docstring Array.foldrM}

Manual/BasicTypes/List.lean

@@ -254,6 +254,10 @@ tag := "list-api-reference"
 
 ## Iteration
 
+{docstring List.iter}
+
+{docstring List.iterM}
+
 {docstring List.forA}
 
 {docstring List.forM}

Manual/BasicTypes/Maps.lean

@@ -449,6 +449,12 @@ $_ ~m $_
 
 ## Iteration
 
+{docstring Std.HashMap.iter}
+
+{docstring Std.HashMap.keysIter}
+
+{docstring Std.HashMap.valuesIter}
+
 {docstring Std.HashMap.map}
 
 {docstring Std.HashMap.fold}
@@ -571,6 +577,12 @@ $_ ~m $_
 
 ## Iteration
 
+{docstring Std.DHashMap.iter}
+
+{docstring Std.DHashMap.keysIter}
+
+{docstring Std.DHashMap.valuesIter}
+
 {docstring Std.DHashMap.map}
 
 {docstring Std.DHashMap.fold}
@@ -812,6 +824,8 @@ $_ ~m $_
 
 ## Iteration
 
+{docstring Std.HashSet.iter}
+
 {docstring Std.HashSet.all}
 
 {docstring Std.HashSet.any}
@@ -972,6 +986,12 @@ The declarations in this section should be imported using `import Std.DTreeMap`.
 
 ## Iteration
 
+{docstring Std.DTreeMap.iter}
+
+{docstring Std.DTreeMap.keysIter}
+
+{docstring Std.DTreeMap.valuesIter}
+
 {docstring Std.DTreeMap.map}
 
 {docstring Std.DTreeMap.foldl}

Manual/BasicTypes/Maps/TreeMap.lean

@@ -219,6 +219,12 @@ The declarations in this section should be imported using `import Std.TreeMap`.
 
 # Iteration
 
+{docstring Std.TreeMap.iter}
+
+{docstring Std.TreeMap.keysIter}
+
+{docstring Std.TreeMap.valuesIter}
+
 {docstring Std.TreeMap.map}
 
 {docstring Std.TreeMap.all}

Manual/BasicTypes/Maps/TreeSet.lean

@@ -127,6 +127,8 @@ tag := "TreeSet"
 
 # Iteration
 
+{docstring Std.TreeSet.iter}
+
 {docstring Std.TreeSet.all}
 
 {docstring Std.TreeSet.any}