OAI/Computability/QuantumFactoring/BitStackBasicProcedures.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.duplicate line 16

   Source documentation

   Duplicate the input word and quote the first copy to represent a pair.

   noncomputable def duplicate (ea : α→List Bool) :
       Procedure ea (prodCode ea ea) (fun a=>(a,a)) where
   …

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure, OAI.ExactQuantumFactoring.BitStackProgram.prodCode

2. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.pair line 51
3. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.first line 56

   Source documentation

   Projection parses the actual prefix code and explicitly clears its tail.

   noncomputable def first (ea : α→List Bool) (eb : β→List Bool) :
       Procedure (prodCode ea eb) ea Prod.fst where
   …

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure, OAI.ExactQuantumFactoring.BitStackProgram.prodCode

4. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.second line 85