OAI/Combinatorics/LowSpaceSubsetSum/Streams/SliceCursor.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Cyclic row cursors into one shared immutable array

Each cursor stores its slice endpoints and the constant-size cyclic state. Reading a row accesses the original array; it does not allocate a row array. Empty slices have no cursor. The list slice and full trace are proof views.

  1. structure OAI.LowSpaceSubsetSum.SliceCursor.Range line 18
  2. structure OAI.LowSpaceSubsetSum.SliceCursor.State line 24
  3. def OAI.LowSpaceSubsetSum.SliceCursor.values line 28
  4. def OAI.LowSpaceSubsetSum.SliceCursor.next line 31
  5. def OAI.LowSpaceSubsetSum.SliceCursor.output line 39
  6. theorem OAI.LowSpaceSubsetSum.SliceCursor.reader line 46
  7. def OAI.LowSpaceSubsetSum.SliceCursor.initial line 57
  8. def OAI.LowSpaceSubsetSum.SliceCursor.slice line 63

    Source documentation

    A slice is a proof view, not a newly allocated row array.

    def slice (xs : Array α) (r : Range xs.size) : List α := List.ofFn (values xs r)

    Mentions: OAI.LowSpaceSubsetSum.SliceCursor.Range, OAI.LowSpaceSubsetSum.SliceCursor.values

  9. theorem OAI.LowSpaceSubsetSum.SliceCursor.initial_perm line 65
  10. theorem OAI.LowSpaceSubsetSum.SliceCursor.initial_length line 76
  11. theorem OAI.LowSpaceSubsetSum.SliceCursor.slice_eq_drop_take line 81
  12. theorem OAI.LowSpaceSubsetSum.SliceCursor.initial_occurrences line 92