OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRouteSelectorProgram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

A literal 140-entry selector checks finite permissions and both physical endpoints. No unbounded search or choice occurs in the resulting program.

  1. abbrev OAI.ContinuumCoulomb.QuantumRouteSelectorProgram.Ends line 14
  2. def OAI.ContinuumCoulomb.QuantumRouteSelectorProgram.endsCode line 15
  3. def OAI.ContinuumCoulomb.QuantumRouteSelectorProgram.accepts line 16
  4. opaque OAI.ContinuumCoulomb.QuantumRouteSelectorProgram.matchProgram line 19
  5. def OAI.ContinuumCoulomb.QuantumRouteSelectorProgram.choose line 34
  6. opaque OAI.ContinuumCoulomb.QuantumRouteSelectorProgram.chooseProgram line 37
  7. abbrev OAI.ContinuumCoulomb.QuantumRouteSelectorProgram.Input line 44
  8. def OAI.ContinuumCoulomb.QuantumRouteSelectorProgram.inputCode line 45
  9. def OAI.ContinuumCoulomb.QuantumRouteSelectorProgram.candidates line 47
  10. opaque OAI.ContinuumCoulomb.QuantumRouteSelectorProgram.candidatesProgram line 50
  11. def OAI.ContinuumCoulomb.QuantumRouteSelectorProgram.value line 63
  12. opaque OAI.ContinuumCoulomb.QuantumRouteSelectorProgram.program line 65
  13. def OAI.ContinuumCoulomb.QuantumRouteSelectorProgram.certificate line 68