Differential checks in the editor

#compare candidate with reference on cases runs pure functions on an explicit, nonempty array. Add using relation to choose the comparison. This is a test command, not a proof tactic. Import NN.Testing.Compare instead for the effectful runner in a compiled executable.

def compareCommand : Lean.ParserDescr

Execute a differential test of pure functions on explicit inputs. This is not a proof.