OAI/MathematicalPhysics/ContinuumCoulomb/Programs/ContactCanonicalEdgeProgram.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The canonical lattice strip is computed by integer comparisons.

  1. def OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.latticeCode line 11
  2. def OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.inputCode line 12
  3. def OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.edgeCode line 13
  4. opaque OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.integerEqual line 17
  5. opaque OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.integerLess line 23
  6. opaque OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.leftProgram line 29
  7. opaque OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.rightProgram line 31
  8. opaque OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.leftXProgram line 33
  9. opaque OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.leftYProgram line 35
  10. opaque OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.rightXProgram line 37
  11. opaque OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.rightYProgram line 39
  12. opaque OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.verticalProgram line 42
  13. opaque OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.forwardProgram line 45
  14. opaque OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.anchorProgram line 50
  15. opaque OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.reverseProgram line 55
  16. opaque OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.program line 59
  17. def OAI.ContinuumCoulomb.ContactCanonicalEdgeProgram.certificate line 63