structure DocGen4.ChunkArray (α : Type u_1) : Type u_1

• array : Array α
• chunkSize : Nat
• curr : Nat
• chunkSize_gt_zero : self.chunkSize > 0
• curr_valid : self.curr ≤ self.array.size

def DocGen4.chunked {α : Type u_1} (xs : Array α) (n : Nat) (ok : n > 0 := by grind) : Std.Iter (Subarray α)

Equations

• DocGen4.chunked xs n ok = { internalState := { array := xs, chunkSize := n, curr := 0, chunkSize_gt_zero := ⋯, curr_valid := ⋯ } }

def DocGen4.ChunkArray.PlausibleStep {α : Type u_1} {m : Type u_1 → Type u_2} (it : Std.IterM m (Subarray α)) (step : Std.IterStep (Std.IterM m (Subarray α)) (Subarray α)) : Prop

Equations

• One or more equations did not get rendered due to their size.
• DocGen4.ChunkArray.PlausibleStep it Std.IterStep.done = (it.internalState.curr = it.internalState.array.size)
• DocGen4.ChunkArray.PlausibleStep it (Std.IterStep.skip it_1) = False

@[implicit_reducible]

instance DocGen4.instIteratorChunkArraySubarrayOfPure {m : Type u_1 → Type u_2} {α : Type u_1} [Pure m] : Std.Iterator (ChunkArray α) m (Subarray α)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance DocGen4.instIteratorLoopChunkArraySubarrayOfMonad {m : Type u_1 → Type u_2} {n : Type u_3 → Type u_4} {α : Type u_1} [Pure m] [Monad n] : Std.IteratorLoop (ChunkArray α) m n

Equations

• DocGen4.instIteratorLoopChunkArraySubarrayOfMonad = Std.IteratorLoop.defaultImplementation