OAI/Computability/QuantumFactoring/NativeAIGVector.lean
13 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ExactQuantumFactoring.NativeAIG.eraseVecline 13 - lemma
OAI.ExactQuantumFactoring.NativeAIG.eraseVec_lengthline 15 - lemma
OAI.ExactQuantumFactoring.NativeAIG.eraseVec_getline 17 - lemma
OAI.ExactQuantumFactoring.NativeAIG.eraseVec_castline 21 - lemma
OAI.ExactQuantumFactoring.NativeAIG.eraseVec_emptyline 23 - lemma
OAI.ExactQuantumFactoring.NativeAIG.eraseVec_pushline 24 - lemma
OAI.ExactQuantumFactoring.NativeAIG.refVec_get_gateline 33 - lemma
OAI.ExactQuantumFactoring.NativeAIG.refVec_get_invertline 36 - def
OAI.ExactQuantumFactoring.NativeAIG.VecRelline 40 - def
OAI.ExactQuantumFactoring.NativeAIG.declIsZeroline 43 - def
OAI.ExactQuantumFactoring.NativeAIG.knownline 46 - def
OAI.ExactQuantumFactoring.NativeAIG.countKnownline 47 - lemma
OAI.ExactQuantumFactoring.NativeAIG.known_eqline 48