The verify(expr1, expr2, symbol) calling sequence returns true if the two symbols "appear the same". The result can be different from that produced by the evalb routine if either symbol has assumptions or is an escaped local.

This verification is symmetric in its arguments.

If either expr1 or expr2 is not of type symbol, then false is returned.

$\mathrm{assume}\left(0<a\right)$

$a,'a',\mathrm{evalb}\left(a='a'\right)$

$\mathrm{a~},a,\mathrm{false}$

$\mathrm{verify}\left(a\&comma;'a'\&comma;\mathrm{symbol}\right)$

$\mathrm{true}$

$f≔\mathrm{convert}\left(b\&comma;\mathrm{`local`}\right)$

$f≔b$

$b,f,\mathrm{evalb}\left(b=f\right)$

$b,b,\mathrm{false}$

$\mathrm{verify}\left(b\&comma;f\&comma;\mathrm{symbol}\right)$

$\mathrm{true}$