(value :q)
(lp)
(certify-book "definline" ? t :ttags '(definline))