OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedLabelProgram.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Polynomial list programs for the literal support-label operations. Only constant-length prefixes are split in the early gadget compiler.

  1. abbrev OAI.ContinuumCoulomb.QuantumOrderedLabelData.labelCode line 13
  2. abbrev OAI.ContinuumCoulomb.QuantumOrderedLabelData.labelsCode line 14
  3. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.takeProgram line 16
  4. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.dropProgram line 28
  5. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.oddLetters line 33
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.oddLetters_eq line 36
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.fold_oddLetters line 50
  8. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.oddProgram line 60
  9. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.axisProgram line 77
  10. abbrev OAI.ContinuumCoulomb.QuantumOrderedLabelData.BlockInput line 83
  11. abbrev OAI.ContinuumCoulomb.QuantumOrderedLabelData.blockCode line 84
  12. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.mediatorProgram line 85
  13. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.labelsProgram line 86
  14. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.prefixProgram line 87
  15. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.suffixProgram line 89
  16. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.mediatorLabelProgram line 91
  17. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.singletonProgram line 94
  18. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.subdivisionProgram line 99