OAI/Analysis/MatrixSigning/Realization/ConditionalRoutine.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.ConditionalRoutine.flag line 12
  2. abbrev OAI.CurrentKS.ConditionalRoutine.work line 13
  3. def OAI.CurrentKS.ConditionalRoutine.ports line 14
  4. def OAI.CurrentKS.ConditionalRoutine.parsePorts line 15
  5. lemma OAI.CurrentKS.ConditionalRoutine.parsePorts_apply line 17
  6. def OAI.CurrentKS.ConditionalRoutine.state line 20
  7. def OAI.CurrentKS.ConditionalRoutine.parse line 22
  8. def OAI.CurrentKS.ConditionalRoutine.select line 23
  9. def OAI.CurrentKS.ConditionalRoutine.choose line 27
  10. def OAI.CurrentKS.ConditionalRoutine.program line 30
  11. lemma OAI.CurrentKS.ConditionalRoutine.parse_spec line 32
  12. lemma OAI.CurrentKS.ConditionalRoutine.choose_true line 40
  13. lemma OAI.CurrentKS.ConditionalRoutine.choose_false line 69
  14. lemma OAI.CurrentKS.ConditionalRoutine.core_spec line 98
  15. def OAI.CurrentKS.ConditionalRoutine.routine line 109