OAI/Computability/QuantumFactoring/ExpressionPostfix.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.NetworkEmission.ExprToken line 19

    Source documentation

    Variables, scalar constants, and the fixed algebra instruction vocabulary.

    abbrev ExprToken (v : Type) := v ⊕ (ℕ ⊕ ℕ)
  2. def OAI.ExactQuantumFactoring.NetworkEmission.exprTokenCode line 20
  3. def OAI.ExactQuantumFactoring.NetworkEmission.pairToken line 21
  4. def OAI.ExactQuantumFactoring.NetworkEmission.compToken line 22
  5. def OAI.ExactQuantumFactoring.NetworkEmission.opToken line 23
  6. def OAI.ExactQuantumFactoring.NetworkEmission.primPack line 24
  7. def OAI.ExactQuantumFactoring.NetworkEmission.tokenOp line 34
  8. def OAI.ExactQuantumFactoring.NetworkEmission.exprRun line 40
  9. lemma OAI.ExactQuantumFactoring.NetworkEmission.exprRun_append line 42
  10. def OAI.ExactQuantumFactoring.NetworkEmission.Produces line 45
  11. lemma OAI.ExactQuantumFactoring.NetworkEmission.produces_var line 47
  12. lemma OAI.ExactQuantumFactoring.NetworkEmission.produces_const line 49
  13. lemma OAI.ExactQuantumFactoring.NetworkEmission.produces_op line 51
  14. lemma OAI.ExactQuantumFactoring.NetworkEmission.produces_pair line 55
  15. lemma OAI.ExactQuantumFactoring.NetworkEmission.produces_binary line 59
  16. def OAI.ExactQuantumFactoring.NetworkEmission.leTokens line 64
  17. def OAI.ExactQuantumFactoring.NetworkEmission.muxTokens line 66
  18. def OAI.ExactQuantumFactoring.NetworkEmission.lePack line 68
  19. lemma OAI.ExactQuantumFactoring.NetworkEmission.produces_le line 69
  20. lemma OAI.ExactQuantumFactoring.NetworkEmission.produces_mux line 73
  21. def OAI.ExactQuantumFactoring.NetworkEmission.exprTokens line 78
  22. def OAI.ExactQuantumFactoring.NetworkEmission.exprPack line 88
  23. lemma OAI.ExactQuantumFactoring.NetworkEmission.exprTokens_produces line 99
  24. lemma OAI.ExactQuantumFactoring.NetworkEmission.lePack_value line 110
  25. lemma OAI.ExactQuantumFactoring.NetworkEmission.exprPack_value line 114