OAI/Combinatorics/LowSpaceSubsetSum/Storage/SamplerFinCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The executable finite-range sampler with its stored candidates

  1. def OAI.LowSpaceSubsetSum.SamplerFinCells.cast line 12
  2. theorem OAI.LowSpaceSubsetSum.SamplerFinCells.cast_value line 16
  3. theorem OAI.LowSpaceSubsetSum.SamplerFinCells.cast_cells line 23
  4. def OAI.LowSpaceSubsetSum.SamplerFinCells.run line 29
  5. theorem OAI.LowSpaceSubsetSum.SamplerFinCells.run_value line 37
  6. theorem OAI.LowSpaceSubsetSum.SamplerFinCells.run_cells line 45