OAI/Analysis/MatrixSigning/Arithmetic/RationalCompareParser.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W06.RationalCompare.fields line 9
  2. def OAI.KS.W06.RationalCompare.leftNumeratorPorts line 12
  3. def OAI.KS.W06.RationalCompare.leftDenominatorPorts line 13
  4. def OAI.KS.W06.RationalCompare.rightNumeratorPorts line 14
  5. def OAI.KS.W06.RationalCompare.rightDenominatorPorts line 15
  6. def OAI.KS.W06.RationalCompare.pairBits line 17
  7. def OAI.KS.W06.RationalCompare.parseProgram line 21
  8. def OAI.KS.W06.RationalCompare.parseTicks line 27
  9. theorem OAI.KS.W06.RationalCompare.parse_spec line 30
  10. def OAI.KS.W06.RationalCompare.constructorBits line 82
  11. def OAI.KS.W06.RationalCompare.negativeBit line 83
  12. theorem OAI.KS.W06.RationalCompare.pairBits_encodeRat line 85
  13. theorem OAI.KS.W06.RationalCompare.pairBits_length line 94