OAI/Combinatorics/KMedian/Binary/NumericParserProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.InputParser.take_poly line 13
  2. theorem OAI.MetricKMedian.InputParser.drop_poly line 14
  3. theorem OAI.MetricKMedian.InputParser.value_poly line 15
  4. theorem OAI.MetricKMedian.InputParser.signed_poly line 16
  5. theorem OAI.MetricKMedian.InputParser.mkRat_poly line 17
  6. def OAI.MetricKMedian.InputParser.width line 18
  7. theorem OAI.MetricKMedian.InputParser.width_poly line 19
  8. def OAI.MetricKMedian.InputParser.natRead line 20
  9. theorem OAI.MetricKMedian.InputParser.natRead_poly line 22
  10. theorem OAI.MetricKMedian.InputParser.prefix_width line 28
  11. theorem OAI.MetricKMedian.InputParser.natRead_append line 32
  12. theorem OAI.MetricKMedian.InputParser.natRead_rest_length line 42
  13. def OAI.MetricKMedian.InputParser.ratRead line 44
  14. theorem OAI.MetricKMedian.InputParser.ratRead_poly line 48
  15. theorem OAI.MetricKMedian.InputParser.ratRead_append line 49
  16. theorem OAI.MetricKMedian.InputParser.ratRead_rest_length line 53