OAI/Combinatorics/KMedian/Binary/InstanceParserProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.InputParser.take_comp line 15
  2. theorem OAI.MetricKMedian.InputParser.drop_comp line 18
  3. def OAI.MetricKMedian.InputParser.squareUnits line 21
  4. theorem OAI.MetricKMedian.InputParser.squareUnits_poly line 22
  5. theorem OAI.MetricKMedian.InputParser.squareUnits_length line 23
  6. def OAI.MetricKMedian.InputParser.reshape line 27
  7. theorem OAI.MetricKMedian.InputParser.reshape_poly line 29
  8. theorem OAI.MetricKMedian.InputParser.flatten_ofFn line 30
  9. theorem OAI.MetricKMedian.InputParser.reshape_flatten line 49
  10. def OAI.MetricKMedian.InputParser.matrix line 67
  11. def OAI.MetricKMedian.InputParser.matrixProgram line 69
  12. theorem OAI.MetricKMedian.InputParser.matrix_encoded line 73
  13. abbrev OAI.MetricKMedian.InputParser.Header line 84
  14. def OAI.MetricKMedian.InputParser.header line 85
  15. theorem OAI.MetricKMedian.InputParser.header_poly line 89
  16. theorem OAI.MetricKMedian.InputParser.header_encoded line 90
  17. def OAI.MetricKMedian.InputParser.raw line 106
  18. def OAI.MetricKMedian.InputParser.rawProgram line 109
  19. theorem OAI.MetricKMedian.InputParser.raw_encoded line 112
  20. def OAI.MetricKMedian.InputParser.instanceProgram line 126