OAI/Combinatorics/KMedian/Binary/SequentialParserProgram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.InputParser.State line 14
  2. def OAI.MetricKMedian.InputParser.parseStep line 15
  3. theorem OAI.MetricKMedian.InputParser.parseStep_poly line 19
  4. def OAI.MetricKMedian.InputParser.parseBound line 26
  5. theorem OAI.MetricKMedian.InputParser.parseFold_size line 29
  6. def OAI.MetricKMedian.InputParser.foldProgram line 54
  7. def OAI.MetricKMedian.InputParser.parse line 87
  8. def OAI.MetricKMedian.InputParser.parseProgram line 90
  9. theorem OAI.MetricKMedian.InputParser.parse_fold_encoded line 96
  10. theorem OAI.MetricKMedian.InputParser.parse_encoded line 109