OAI/Computability/MatchingCount/ListNumeric.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryMatching.StackCode.code_option_none line 10
  2. lemma OAI.BinaryMatching.StackCode.code_option_some line 11
  3. lemma OAI.BinaryMatching.StackCode.fold_code_additive line 16
  4. theorem OAI.BinaryMatching.StackCode.Poly.listFoldAdd line 33
  5. theorem OAI.BinaryMatching.StackCode.Poly.listDrop line 44
  6. theorem OAI.BinaryMatching.StackCode.Poly.listGetD line 62
  7. theorem OAI.BinaryMatching.StackCode.Poly.listNatSum line 66
  8. theorem OAI.BinaryMatching.StackCode.Poly.listIntSum line 72
  9. def OAI.BinaryMatching.StackCode.rangeStep line 84
  10. lemma OAI.BinaryMatching.StackCode.rangeStep_iterate line 85
  11. theorem OAI.BinaryMatching.StackCode.Poly.listRange line 93