OAI/Computability/QuantumFactoring/BitStackConstants.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   A fixed finite list is part of the program, not a run-time oracle.

   def pushWord (k : K) : List Bool→Program K
     | []=>.skip
     | b::bs=>.seq (pushWord k bs) (.push k b)

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Program

2. lemma OAI.ExactQuantumFactoring.BitStackProgram.pushWord_runs line 17
3. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.constant line 27
4. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.quote line 46
5. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.length line 63

   Source documentation

   Count each actual symbol, returning a unary length.

   noncomputable def length : Procedure (id : List Bool→List Bool)
       (fun n=>List.replicate n true) List.length where
   …

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure