OAI/Computability/QuantumFactoring/BitStackQuotation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BitStackProgram.quoteBits line 14

    Source documentation

    Prefix-free quoting for one Boolean word. Both constructor tags and payload bits are literal stack symbols. It is used only by the classical generator.

    def quoteBits (xs : List Bool) : List Bool :=
…
  2. lemma OAI.ExactQuantumFactoring.BitStackProgram.quoteBits_nil line 16
  3. lemma OAI.ExactQuantumFactoring.BitStackProgram.quoteBits_cons line 17
  4. lemma OAI.ExactQuantumFactoring.BitStackProgram.quoteBits_length line 19
  5. def OAI.ExactQuantumFactoring.BitStackProgram.pairBits line 24
  6. lemma OAI.ExactQuantumFactoring.BitStackProgram.pairBits_length line 25
  7. def OAI.ExactQuantumFactoring.BitStackProgram.quoteLoop line 30
  8. def OAI.ExactQuantumFactoring.BitStackProgram.quoteMove line 32
  9. lemma OAI.ExactQuantumFactoring.BitStackProgram.quoteLoop_runs line 35
  10. lemma OAI.ExactQuantumFactoring.BitStackProgram.quoteMove_runs line 67
  11. def OAI.ExactQuantumFactoring.BitStackProgram.unquoteBody line 90
  12. def OAI.ExactQuantumFactoring.BitStackProgram.unquoteLoop line 94
  13. def OAI.ExactQuantumFactoring.BitStackProgram.unquoteMove line 96
  14. lemma OAI.ExactQuantumFactoring.BitStackProgram.unquoteLoop_runs line 99
  15. lemma OAI.ExactQuantumFactoring.BitStackProgram.unquoteMove_runs line 143