OAI/Algebra/FormulaHitting/BitModel.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NCHitting.BitModel.width line 9
  2. def OAI.NCHitting.BitModel.addCost line 11
  3. def OAI.NCHitting.BitModel.mulCost line 12
  4. def OAI.NCHitting.BitModel.compareCost line 13
  5. def OAI.NCHitting.BitModel.listBits line 15
  6. structure OAI.NCHitting.BitModel.NatResult line 17
  7. def OAI.NCHitting.BitModel.powerRun line 22
  8. theorem OAI.NCHitting.BitModel.powerRun_value line 29
  9. inductive OAI.NCHitting.BitModel.Expr line 34
  10. def OAI.NCHitting.BitModel.Expr.run line 46
  11. structure OAI.NCHitting.BitModel.RationalCode line 82
  12. def OAI.NCHitting.BitModel.RationalCode.bits line 88
  13. def OAI.NCHitting.BitModel.outputBits line 91
  14. inductive OAI.NCHitting.BitModel.Program line 93
  15. structure OAI.NCHitting.BitModel.ProgramResult line 101
  16. def OAI.NCHitting.BitModel.Program.run line 106
  17. def OAI.NCHitting.BitModel.execute line 131