zDefine
bossLib.zDefine : term quotation -> thm
General-purpose function definition facility.
zDefine behaves exactly like Define, except that it does not add the
definition to computeLib.the_compset. Consequently the definition is
not used by bossLib.EVAL when evaluating expressions.
Failure
zDefine and Define succeed and fail in the same way.
Example
> zDefine `foo = 10 ** 10 ** 10`
val it = ⊢ foo = 10 ** 10 ** 10: thm
> EVAL ``foo``;
val it = ⊢ foo = foo: thm
Comments
zDefine is helpful when users wish to derive and use their own
efficient evaluation theorems, which can be added using
computeLib.add_funs or computeLib.add_persistent_funs.