OAI/Combinatorics/KMedian/Binary/BinaryListSelection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Binary.ListFindIdx.enc line 16
  2. def OAI.MetricKMedian.Binary.ListFindIdx.body line 17
  3. def OAI.MetricKMedian.Binary.ListFindIdx.result line 19
  4. def OAI.MetricKMedian.Binary.ListFindIdx.program line 20
  5. theorem OAI.MetricKMedian.Binary.ListFindIdx.run line 30
  6. def OAI.MetricKMedian.Binary.ListFindIdx.loop line 53
  7. theorem OAI.MetricKMedian.Binary.ListAlgorithms.foldChoice line 64
  8. def OAI.MetricKMedian.Binary.PolyProgram.listFindIdx line 79
  9. def OAI.MetricKMedian.Binary.PolyProgram.listChoose line 83