Ed25519.equal: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as Ed25519
Lines 188-192 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend&start_line=188&end_line=192

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS

# the same point: X1 Z2 == X2 Z1 and Y1 Z2 == Y2 Z1
def equal(+p: Nat, a: EPt, b: EPt) -> Bool:
  match a b:
    case EPt{+x1, +y1, +z1, t1} EPt{+x2, +y2, +z2, t2}:
      Bool.and(Nat.is_eq(FS.fmul(p, x1, z2), FS.fmul(p, x2, z1)), Nat.is_eq(FS.fmul(p, y1, z2), FS.fmul(p, y2, z1)))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend&name=fmul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend&name=EPt