OAI/Combinatorics/ThinTrees/Arithmetic/ScalarRealization.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Scalar realization.

  1. abbrev OAI.CurrentKS.Realization.SquareScan line 17
  2. abbrev OAI.CurrentKS.Realization.squareScanCode line 18
  3. abbrev OAI.CurrentKS.Realization.squarePayload line 19
  4. abbrev OAI.CurrentKS.Realization.squareRest line 20
  5. abbrev OAI.CurrentKS.Realization.squarePower line 21
  6. abbrev OAI.CurrentKS.Realization.squareAccum line 22
  7. def OAI.CurrentKS.Realization.squareScanStep line 24
  8. def OAI.CurrentKS.Realization.squareScan line 27
  9. instance OAI.CurrentKS.Realization.poly_squareScan line 32
  10. lemma OAI.CurrentKS.Realization.squareScan_correct line 37
  11. lemma OAI.CurrentKS.Realization.squareScan_invariant line 54
  12. instance OAI.CurrentKS.Realization.size_squareScan line 78
  13. def OAI.CurrentKS.Realization.scalarFactorProgram line 105
  14. instance OAI.CurrentKS.Realization.poly_scalarFactorProgram line 115