Reconstruction.validate: def of bend-edit-distance@0.2.2.0
Import: import bend-edit-distance@0.2.2.0/src/Reconstruction.bend as Reconstruction
Lines 231-249 of bend-edit-distance@0.2.2.0/src/Reconstruction.bend: https://jend.leeeet.dev/read.txt?path=bend-edit-distance@0.2.2.0/src/Reconstruction.bend&start_line=231&end_line=249

import Base
import bend-edit-distance@0.2.2.0/EdlibTypes.bend as E

# Edlib codes: Match=0 consumes both, Insert=1 consumes query only,
# Delete=2 consumes target only, Mismatch=3 consumes both. Validation requires
# exact consumption, the configured (symmetric, nontransitive) predicate on
# every diagonal operation, and an edit cost equal to the reported distance.
def validate(operations: List<&2, E.Operation>, query: String, target: String,
               +pairs: List<&2, E.EqualityPair>, +expected: Nat, cost: Nat) -> Bool:
  match operations query target:
    case Nil{} SNil{} SNil{}:
      Nat.is_eq(cost, expected)
    case E.Match{} <> tail SCon{q, qt} SCon{t, tt}:
      Bool.and(E.equal(pairs, q, t), validate(tail, qt, tt, pairs, expected, cost))
    case E.Mismatch{} <> tail SCon{q, qt} SCon{t, tt}:
      Bool.and(Bool.not(E.equal(pairs, q, t)), validate(tail, qt, tt, pairs, expected, 1n+cost))
    case E.Insert{} <> tail SCon{_, qt} _:
      validate(tail, qt, target, pairs, expected, 1n+cost)
    case E.Delete{} <> tail _ SCon{_, tt}:
      validate(tail, query, tt, pairs, expected, 1n+cost)
    case _ _ _:
      False{}

Uses (10):
  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=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=bend-edit-distance@0.2.2.0/EdlibTypes.bend&name=EqualityPair
  https://jend.leeeet.dev/definition.txt?path=bend-edit-distance@0.2.2.0/EdlibTypes.bend&name=Operation
  https://jend.leeeet.dev/definition.txt?path=bend-edit-distance@0.2.2.0/EdlibTypes.bend&name=equal