OAI/Analysis/MatrixSigning/Encoding/DenseCanonicalParser.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.DenseCanonicalParser.state line 10
  2. def OAI.CurrentKS.DenseCanonicalParser.headerPorts line 14
  3. def OAI.CurrentKS.DenseCanonicalParser.copyPorts line 15
  4. def OAI.CurrentKS.DenseCanonicalParser.counterPorts line 16
  5. def OAI.CurrentKS.DenseCanonicalParser.matrixPorts line 17
  6. def OAI.CurrentKS.DenseCanonicalParser.header line 18
  7. def OAI.CurrentKS.DenseCanonicalParser.saveDimension line 19
  8. def OAI.CurrentKS.DenseCanonicalParser.counter line 20
  9. def OAI.CurrentKS.DenseCanonicalParser.matrices line 21
  10. def OAI.CurrentKS.DenseCanonicalParser.body line 22
  11. def OAI.CurrentKS.DenseCanonicalParser.program line 23
  12. lemma OAI.CurrentKS.DenseCanonicalParser.header_spec line 25
  13. lemma OAI.CurrentKS.DenseCanonicalParser.saveDimension_spec line 40
  14. lemma OAI.CurrentKS.DenseCanonicalParser.counter_spec line 48
  15. lemma OAI.CurrentKS.DenseCanonicalParser.matrices_spec line 61
  16. def OAI.CurrentKS.DenseCanonicalParser.ticks line 77
  17. theorem OAI.CurrentKS.DenseCanonicalParser.program_spec line 82
  18. lemma OAI.CurrentKS.DenseCanonicalParser.binaryDimension_le_length line 93
  19. lemma OAI.CurrentKS.DenseCanonicalParser.ticks_le_polynomial line 98