OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumHistoryTableProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Total local-table dispatcher for the literal history order. Its seven arity templates are fixed; only descriptor and short-label reads vary.

  1. abbrev OAI.ContinuumCoulomb.QuantumHistoryTableProgram.Input line 16
  2. def OAI.ContinuumCoulomb.QuantumHistoryTableProgram.inputCode line 17
  3. def OAI.ContinuumCoulomb.QuantumHistoryTableProgram.localTable line 20
  4. opaque OAI.ContinuumCoulomb.QuantumHistoryTableProgram.circuitProgram line 28
  5. opaque OAI.ContinuumCoulomb.QuantumHistoryTableProgram.restProgram line 30
  6. opaque OAI.ContinuumCoulomb.QuantumHistoryTableProgram.indexProgram line 32
  7. opaque OAI.ContinuumCoulomb.QuantumHistoryTableProgram.labelsProgram line 34
  8. opaque OAI.ContinuumCoulomb.QuantumHistoryTableProgram.descriptorProgram line 36
  9. opaque OAI.ContinuumCoulomb.QuantumHistoryTableProgram.cutoffProgram line 39
  10. opaque OAI.ContinuumCoulomb.QuantumHistoryTableProgram.localTableProgram line 43
  11. def OAI.ContinuumCoulomb.QuantumHistoryTableProgram.table line 60
  12. opaque OAI.ContinuumCoulomb.QuantumHistoryTableProgram.tableProgram line 68
  13. theorem OAI.ContinuumCoulomb.QuantumHistoryTableProgram.table_eq line 81
  14. def OAI.ContinuumCoulomb.QuantumHistoryTableProgram.certificate line 85