OAI/Computability/DepthThree/LanguageParser.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DepthThreeLowerBound.ParsedInput line 8
  2. def OAI.DepthThreeLowerBound.decodeInput line 17
  3. def OAI.DepthThreeLowerBound.InputFits line 27
  4. instance OAI.DepthThreeLowerBound.(instance at line 32) line 32
  5. def OAI.DepthThreeLowerBound.parseInput line 36
  6. theorem OAI.DepthThreeLowerBound.parseInput_of_fits line 39
  7. theorem OAI.DepthThreeLowerBound.parseInput_of_not_fits line 43
  8. theorem OAI.DepthThreeLowerBound.parseInput_eq_some_iff line 47
  9. theorem OAI.DepthThreeLowerBound.parseInput_eq_none_iff line 53
  10. theorem OAI.DepthThreeLowerBound.decodeInput_dataSize line 59
  11. theorem OAI.DepthThreeLowerBound.decodeInput_ringDegree line 62
  12. theorem OAI.DepthThreeLowerBound.decodeInput_coefficientCount line 65
  13. theorem OAI.DepthThreeLowerBound.data_read_lt line 68
  14. theorem OAI.DepthThreeLowerBound.hash_read_lt line 72
  15. theorem OAI.DepthThreeLowerBound.polynomial_read_lt line 81
  16. theorem OAI.DepthThreeLowerBound.coefficient_read_lt line 87
  17. theorem OAI.DepthThreeLowerBound.decoded_ringDegree_pos line 93
  18. theorem OAI.DepthThreeLowerBound.decoded_coefficientCount_two_le line 97