OAI/Computability/QuantumFactoring/NativeAIGModel.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.NativeAIG.Ref line 11
  2. abbrev OAI.ExactQuantumFactoring.NativeAIG.Key line 12
  3. inductive OAI.ExactQuantumFactoring.NativeAIG.Decl line 15

    Source documentation

    A literal list representation of the nodes and the (possibly incomplete) cache. The cache is not replaced by a search through all nodes.

    inductive Decl where
…
  4. structure OAI.ExactQuantumFactoring.NativeAIG.Graph line 20
  5. def OAI.ExactQuantumFactoring.NativeAIG.eraseDecl line 25
  6. def OAI.ExactQuantumFactoring.NativeAIG.lookup line 29
  7. def OAI.ExactQuantumFactoring.NativeAIG.nativeKey line 33
  8. def OAI.ExactQuantumFactoring.NativeAIG.Rel line 35
  9. def OAI.ExactQuantumFactoring.NativeAIG.constant line 38
  10. def OAI.ExactQuantumFactoring.NativeAIG.empty line 43
  11. def OAI.ExactQuantumFactoring.NativeAIG.atom line 44
  12. def OAI.ExactQuantumFactoring.NativeAIG.addGate line 46
  13. def OAI.ExactQuantumFactoring.NativeAIG.go line 48
  14. def OAI.ExactQuantumFactoring.NativeAIG.gate line 59
  15. def OAI.ExactQuantumFactoring.NativeAIG.EPRel line 62
  16. lemma OAI.ExactQuantumFactoring.NativeAIG.cache_project line 65
  17. lemma OAI.ExactQuantumFactoring.NativeAIG.nativeKey_injective line 70
  18. lemma OAI.ExactQuantumFactoring.NativeAIG.empty_rel line 79
  19. lemma OAI.ExactQuantumFactoring.NativeAIG.constant_eq line 83
  20. lemma OAI.ExactQuantumFactoring.NativeAIG.atom_rel line 91
  21. lemma OAI.ExactQuantumFactoring.NativeAIG.pushed_rel line 98
  22. lemma OAI.ExactQuantumFactoring.NativeAIG.go_rel line 112
  23. lemma OAI.ExactQuantumFactoring.NativeAIG.gate_rel line 153