OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumUnaryPrefixRun.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Exact prefix parsing and emission for the verifier wrapper.

  1. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.next_some line 14
  2. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.tapes_input line 17
  3. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.tapes_saved line 21
  4. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.tapes_temp line 25
  5. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.tapes_source line 29
  6. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.update_input line 33
  7. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.update_saved line 42
  8. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.update_temp line 51
  9. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.parse_cons line 60
  10. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.parse_zero line 74
  11. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.parse_steps line 88
  12. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.emit_delimiter line 102
  13. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.emit_cons line 115
  14. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.emit_zero line 129
  15. theorem OAI.ContinuumCoulomb.QuantumUnaryPrefix.emit_steps line 142