Api.same_eq: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
Lines 224-248 of bendtorch-core@0.1.0.0/src/storage/api.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&start_line=224&end_line=248

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model

def same_eq(+d: Nat, +p: Model.Path(d), +q: Model.Path(d)) ->
  {Nat.is_eq(Model.offset(d, p), Model.offset(d, q)) == Model.same(d, p, q) : Bool}:
  match d:
    case 0n:
      {==}
    case 1n+r:
      Model.Step{+pb, +pr} = p
      match pb:
        case False{}:
          Model.Step{+qb, +qr} = q
          match qb:
            case False{}:
              same_eq(r, pr, qr)
            case True{}:
              Equal.sym(Bool, False{}, Nat.is_eq(Model.offset(r, pr), Nat.add(Model.capacity(r), Model.offset(r, qr))),
                ne_low(Model.offset(r, pr), Model.capacity(r), Model.offset(r, qr), offset_lt(r, pr)))
        case True{}:
          Model.Step{+qb, +qr} = q
          match qb:
            case False{}:
              Equal.sym(Bool, False{}, Nat.is_eq(Nat.add(Model.capacity(r), Model.offset(r, pr)), Model.offset(r, qr)),
                ne_high(Model.offset(r, qr), Model.capacity(r), Model.offset(r, pr), offset_lt(r, qr)))
            case True{}:
              %eq_add_cancel(Model.capacity(r), Model.offset(r, pr), Model.offset(r, qr)) : {_ == Model.same(r, pr, qr) : Bool}
              same_eq(r, pr, qr)

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=eq_add_cancel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=ne_high
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=ne_low
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=offset_lt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Path
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=capacity
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=same