Differential checks on an explicit corpus

compareOn runs two implementations on the same inputs. A mismatch reports the zero-based case index, input, and both results. Callers choose the comparison: exact equality, floating-point bit identity, or a domain-specific tolerance. In particular, no tolerance or NaN policy is implicit.

NN.Testing.Command provides the editor command for pure functions. Keep the reference independent of the implementation being tested. These checks execute code; they do not produce proofs.

def NN.Testing.compareOn {α β γ : Type} [Repr α] [Repr β] [Repr γ] (cases : Array α) (candidate : α → IO β) (reference : α → IO γ) (agrees : β → γ → Bool) : IO Unit

Compare effectful implementations on a nonempty, caller-supplied corpus. The reference runs first; each side must start from equivalent state if it is stateful. Exceptions and empty corpora fail the check rather than count as agreement.