OAI/Algebra/FormulaHitting/Specification.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.NCHittingSpecification.Formula line 13
  2. def OAI.NCHittingSpecification.Formula.gates line 21
  3. def OAI.NCHittingSpecification.Formula.coefficient line 27
  4. def OAI.NCHittingSpecification.Formula.evaluate line 36
  5. def OAI.NCHittingSpecification.dimension line 46
  6. def OAI.NCHittingSpecification.expectedEntry line 49
  7. def OAI.NCHittingSpecification.UniversalHitting line 57
  8. def OAI.NCHittingSpecification.expectedProgram line 65
  9. def OAI.NCHittingSpecification.expectedCode line 78
  10. def OAI.NCHittingSpecification.expectedOutput line 82
  11. def OAI.NCHittingSpecification.decode line 88
  12. def OAI.NCHittingSpecification.entryBitBound line 91
  13. def OAI.NCHittingSpecification.costBound line 93
  14. def OAI.NCHittingSpecification.primitiveBitBound line 109
  15. def OAI.NCHittingSpecification.CompleteClaim line 111
  16. def OAI.NCHittingSpecification.CompleteTheorem line 130