Major Section: OTHER
Examples: (certify-book! "my-arith" 3) ;Certify in a world with 3 ; commands, starting in a world ; with at least 3 commands. (certify-book! "my-arith") ;Certify in the initial world.where
General Form: (certify-book! book-name k compile-flg)
book-nameis a book name (see book-name),
kis a nonnegative integer used to indicate the ``certification world,'' and
compile-flgindicates whether you wish to compile the (functions in the) book. As with
compile-flgis coerced to
nilif explicit compilation is suppressed; see compilation.
This command is identical to
certify-book, except that the second
k may not be
certify-book! and if
exceeds the current command number, then an appropriate
be executed first. See certify-book and see ubt!.