OAI/Analysis/MatrixSigning/Realization/CompareRoutine.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.CompareRoutine.encode line 11
  2. def OAI.CurrentKS.CompareRoutine.parsed line 13
  3. def OAI.CurrentKS.CompareRoutine.decode line 15
  4. def OAI.CurrentKS.CompareRoutine.prepend line 16
  5. def OAI.CurrentKS.CompareRoutine.extract line 17
  6. def OAI.CurrentKS.CompareRoutine.program line 18
  7. lemma OAI.CurrentKS.CompareRoutine.decode_spec line 20
  8. lemma OAI.CurrentKS.CompareRoutine.prepend_spec line 25
  9. lemma OAI.CurrentKS.CompareRoutine.extract_spec line 31
  10. def OAI.CurrentKS.CompareRoutine.ticks line 37
  11. def OAI.CurrentKS.CompareRoutine.routine line 41