OAI/Combinatorics/KMedian/Binary/BinaryListIndex.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Binary.ListSplit.enc line 15
  2. abbrev OAI.MetricKMedian.Binary.ListSplit.out line 16
  3. def OAI.MetricKMedian.Binary.ListSplit.body line 17
  4. def OAI.MetricKMedian.Binary.ListSplit.result line 20
  5. def OAI.MetricKMedian.Binary.ListSplit.program line 21
  6. theorem OAI.MetricKMedian.Binary.ListSplit.run line 33
  7. def OAI.MetricKMedian.Binary.ListSplit.loop line 60
  8. def OAI.MetricKMedian.Binary.PolyProgram.listSplitAt line 72
  9. def OAI.MetricKMedian.Binary.PolyProgram.listTake line 78
  10. def OAI.MetricKMedian.Binary.PolyProgram.listDrop line 81
  11. def OAI.MetricKMedian.Binary.PolyProgram.listGetD line 84
  12. def OAI.MetricKMedian.Binary.PolyProgram.listEraseIdx line 88
  13. def OAI.MetricKMedian.Binary.PolyProgram.listInsertAt line 91