OAI/Analysis/MatrixSigning/Realization/IterateRoutine.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.IterateRoutine.counter line 14
  2. abbrev OAI.CurrentKS.IterateRoutine.work line 15
  3. def OAI.CurrentKS.IterateRoutine.corePorts line 16
  4. def OAI.CurrentKS.IterateRoutine.parsePorts line 17
  5. lemma OAI.CurrentKS.IterateRoutine.parsePorts_apply line 19
  6. def OAI.CurrentKS.IterateRoutine.state line 22
  7. def OAI.CurrentKS.IterateRoutine.parse line 24
  8. def OAI.CurrentKS.IterateRoutine.body line 25
  9. def OAI.CurrentKS.IterateRoutine.program line 27
  10. def OAI.CurrentKS.IterateRoutine.input line 29
  11. lemma OAI.CurrentKS.IterateRoutine.parse_spec line 32
  12. lemma OAI.CurrentKS.IterateRoutine.element_spec line 49
  13. lemma OAI.CurrentKS.IterateRoutine.pop_spec line 63
  14. def OAI.CurrentKS.IterateRoutine.loopTicks line 73
  15. lemma OAI.CurrentKS.IterateRoutine.loop_trace line 77
  16. def OAI.CurrentKS.IterateRoutine.routine line 94
  17. lemma OAI.CurrentKS.IterateRoutine.loopTicks_le line 102