OAI/Combinatorics/MatchingCount/Machines/TreeListOps.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.TreeTyped.listCase line 12
  2. def OAI.MatchingFPRAS.TreeTyped.head line 29
  3. def OAI.MatchingFPRAS.TreeTyped.tail line 32
  4. def OAI.MatchingFPRAS.TreeTyped.isEmpty line 34
  5. def OAI.MatchingFPRAS.TreeTyped.dropStep line 36
  6. lemma OAI.MatchingFPRAS.TreeTyped.countDown_drop line 38
  7. def OAI.MatchingFPRAS.TreeTyped.drop line 45
  8. def OAI.MatchingFPRAS.TreeTyped.getD line 48
  9. def OAI.MatchingFPRAS.TreeTyped.mapStep line 54
  10. def OAI.MatchingFPRAS.TreeTyped.mapStepRealizer line 56
  11. lemma OAI.MatchingFPRAS.TreeTyped.mapStep_fold line 62
  12. def OAI.MatchingFPRAS.TreeTyped.mapWith line 71
  13. def OAI.MatchingFPRAS.TreeTyped.map line 79
  14. def OAI.MatchingFPRAS.TreeTyped.listLength line 86
  15. def OAI.MatchingFPRAS.TreeTyped.append line 97
  16. def OAI.MatchingFPRAS.TreeTyped.filter line 103