OAI/Analysis/MatrixSigning/Realization/RatFieldsRealization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Realization.wordTail line 13
  2. abbrev OAI.CurrentKS.Realization.numFieldsCode line 23
  3. def OAI.CurrentKS.Realization.ratFields line 25
  4. def OAI.CurrentKS.Realization.ratNumBinary line 35
  5. def OAI.CurrentKS.Realization.unframeNat line 38
  6. def OAI.CurrentKS.Realization.ratDenBinary line 42
  7. def OAI.CurrentKS.Realization.binaryToNat line 45
  8. def OAI.CurrentKS.Realization.wordLength line 58
  9. def OAI.CurrentKS.Realization.binarySize line 74
  10. def OAI.CurrentKS.Realization.ratDenSize line 78
  11. def OAI.CurrentKS.Realization.ratNumToNat line 80
  12. def OAI.CurrentKS.Realization.ratCeil line 94