OAI/MathematicalPhysics/ContinuumCoulomb/Programs/ContactRationalPlaceProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Exact strip placement uses only rational arithmetic and the two computed orientation bits. It preserves the original lattice endpoints.

  1. abbrev OAI.ContinuumCoulomb.ContactRationalPlaceProgram.Input line 13
  2. def OAI.ContinuumCoulomb.ContactRationalPlaceProgram.inputCode line 15
  3. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.edgeProgram line 18
  4. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.pointProgram line 21
  5. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.verticalProgram line 24
  6. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.edgeTailProgram line 30
  7. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.reverseProgram line 37
  8. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.anchorProgram line 41
  9. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.anchorXProgram line 45
  10. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.anchorYProgram line 49
  11. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.rawXProgram line 53
  12. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.rawYProgram line 56
  13. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.reflectedXProgram line 59
  14. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.baseXProgram line 64
  15. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.baseYProgram line 68
  16. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.xProgram line 72
  17. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.yProgram line 79
  18. opaque OAI.ContinuumCoulomb.ContactRationalPlaceProgram.program line 87
  19. def OAI.ContinuumCoulomb.ContactRationalPlaceProgram.certificate line 94