AddVerification adds a new verification verificationname into the verification system.

The handler argument is either a procedure, appliable module, or a structured verification describing the new verification.

If handler is a procedure, then a call to verify of the form verify( expr1, expr2, verificationname ) results in a call to handler( expr1, expr2 ). Additional arguments can be passed to handler from a call to verify of the form $\mathrm{verify}\left(\mathrm{expr1},\mathrm{expr2},\mathrm{verificationname}\left(\mathrm{arg1},\mathrm{arg2},...\right)\right)$, which results in the call $\mathrm{handler}\left(\mathrm{expr1},\mathrm{expr2},\mathrm{arg1},\mathrm{arg2},...\right)$. The handler argument, if it is a procedure, must return either true, false, FAIL, [false, result], or [FAIL, result], where result is some expression or expression sequence which provides some information relating to or explaining the failure. It must also be prepared to handle any argument sequence that is passed to it.

If the handler argument is a structured verification, then the verification test is defined by the structured verification interpreter as though the structured verification were used directly in a call to verify.

Exists(verificationname) checks whether there is a verification named verificationname in the verification system. It returns true if so and false otherwise.

GetVerification(verificationname) returns the value of the verification named verificationname if it exists in the verification system.

GetVerifications() returns the list of verifications in the verification system. GetVerifications(`global`) returns the sublist of known verifications which have global names. GetVerifications(`local`) returns the sublist of known verifications whose names are not global.

RemoveVerification(verificationname) removes the verification verificationname from the verification system.

The AddVerification and RemoveVerification commands return NULL.

$\mathrm{with}\left(\mathrm{VerifyTools}\right)\:$

$\mathrm{AddVerification}\left(\mathrm{length\_not\_increased}\,\left(a\,b\right)\mapsto \mathrm{evalb}\left(\mathrm{length}\left(a\right)\le \mathrm{length}\left(b\right)\right)\right)$

$\mathrm{verify}\left(x+\frac{1}{x}\,\frac{x^2+1}{x}\,\mathrm{length\_not\_increased}\right)$

$\mathrm{true}$

$\mathrm{verify}\left(\frac{x^2+1}{x}\,x+\frac{1}{x}\,\mathrm{length\_not\_increased}\right)$

$\mathrm{false}$

$\mathrm{AddVerification}\left(\mathrm{basic}\,\mathrm{And}\left(\mathrm{normal}\,\mathrm{length\_not\_increased}\right)\right)$

$\mathrm{verify}\left(x+\frac{1}{x}\,\frac{x^2+1}{x}\,\mathrm{basic}\right)$

$\mathrm{true}$

$\mathrm{verify}\left(\frac{x^2+1}{x}\,x+\frac{1}{x}\,\mathrm{basic}\right)$

$\mathrm{false}$

$\mathrm{verify}\left(x+1\,\frac{x^2+1}{x}\,\mathrm{basic}\right)$

$\mathrm{false}$

$\mathrm{GetVerification}\left(\mathrm{length\_not\_increased}\right)$

$\left(a\,b\right)\mapsto \mathrm{evalb}\left(\mathrm{length}\left(a\right)\le \mathrm{length}\left(b\right)\right)$

$\mathrm{Exists}\left(\mathrm{basic}\right)$

$\mathrm{true}$

$\mathrm{RemoveVerification}\left(\mathrm{basic}\right)$

$\mathrm{Exists}\left(\mathrm{basic}\right)$

$\mathrm{false}$

$\mathrm{GetVerifications}\left(\right)$

$\left[\mathrm{\&under}\,\mathrm{Array}\,\mathrm{FAIL}\,\mathrm{FrobeniusGroupId}\,\mathrm{Global}\,\mathrm{Matrix}\,\mathrm{MultiSet}\,\mathrm{PermGroup}\,\mathrm{RootOf}\,\mathrm{SmallGroupId}\,\mathrm{Vector}\,\mathrm{address}\,\mathrm{after}\,\mathrm{approx}\,\mathrm{array}\,\mathrm{as\_list}\,\mathrm{as\_multiset}\,\mathrm{as\_set}\,\mathrm{attributes}\,\mathrm{boolean}\,\mathrm{box}\,\mathrm{cbox}\,\mathrm{curve}\,\mathrm{curves}\,\mathrm{dataframe}\,\mathrm{dataseries}\,\mathrm{default}\,\mathrm{default}\,\mathrm{dummyvariable}\,\mathrm{equal}\,\mathrm{evala}\,\mathrm{evalc}\,\mathrm{expand}\,\mathrm{false}\,\mathrm{float}\,\mathrm{function}\,\mathrm{function\_bounds}\,\mathrm{function\_curve}\,\mathrm{function\_shells}\,\mathrm{greater\_equal}\,\mathrm{greater\_than}\,\mathrm{in\_convex\_polygon}\,\mathrm{indef\_int}\,\mathrm{interval}\,\mathrm{length\_not\_increased}\,\mathrm{less\_equal}\,\mathrm{less\_than}\,\mathrm{list}\,\mathrm{listlist}\,\mathrm{matrix}\,\mathrm{member}\,\mathrm{multiset}\,\mathrm{neighborhood}\,\mathrm{neighbourhood}\,\mathrm{normal}\,\mathrm{permute\_elements}\,\mathrm{plot}\,\mathrm{plot3d}\,\mathrm{plot\_distance}\,\mathrm{plotthing\_compile\_result}\,\mathrm{polynom}\,\mathrm{procedure}\,\mathrm{ptbox}\,\mathrm{range}\,\mathrm{rational}\,\mathrm{record}\,\mathrm{relation}\,\mathrm{reverse}\,\mathrm{rifset}\,\mathrm{rifsimp}\,\mathrm{rtable}\,\mathrm{set}\,\mathrm{sign}\,\mathrm{simplify}\,\mathrm{sublist}\,\mathrm{subset}\,\mathrm{subtype}\,\mathrm{superlist}\,\mathrm{superset}\,\mathrm{supertype}\,\mathrm{symbol}\,\mathrm{table}\,\mathrm{table\_indices}\,\mathrm{testeq}\,\mathrm{text}\,\mathrm{true}\,\mathrm{truefalse}\,\mathrm{type}\,\mathrm{undefined}\,\mathrm{units}\,\mathrm{vector}\,\mathrm{verifyfunc}\,\mathrm{wildcard}\,\mathrm{xmltree}\,\mathrm{xvm}\right]$

$\mathrm{Complexity}≔\mathbf{module}\left(\right)\mathrm{\_export}\left(\mathrm{Length}\&comma;\mathrm{NumFunctions}\&comma;\mathrm{NumVars}\right)\&semi;\mathrm{VerifyTools}:-\mathrm{AddVerification}\left(\mathrm{Length}\&comma;\left(a\&comma;b\right)\&rarr;\mathrm{evalb}\left(\mathrm{length}\left(a\right)<=\mathrm{length}\left(b\right)\right)\right)\&semi;\mathrm{VerifyTools}:-\mathrm{AddVerification}\left(\mathrm{NumVars}\&comma;\left(a\&comma;b\right)\&rarr;\mathrm{evalb}\left(\mathrm{numelems}\left(\mathrm{indets}\left(a\&comma;\&apos;\mathrm{name}\&apos;\right)\right)<=\mathrm{numelems}\left(\mathrm{indets}\left(b\&comma;\&apos;\mathrm{name}\&apos;\right)\right)\right)\right)\mathbf{end\; module}\&colon;$

$\mathrm{verify}\left(x+y\&comma;x^2+1\&comma;\mathrm{Complexity}:-\mathrm{Length}\right)$

$\mathrm{true}$

$\mathrm{verify}\left(x+y\&comma;x^2+1\&comma;\mathrm{Complexity}:-\mathrm{NumVars}\right)$

$\mathrm{false}$

$\mathrm{GetVerifications}\left(\mathrm{`local`}\right)$

$\left[\mathrm{Length}\&comma;\mathrm{NumVars}\&comma;\mathrm{curve}\&comma;\mathrm{curves}\&comma;\mathrm{default}\&comma;\mathrm{default}\right]$