For the types of term, rule and declaration, the print representation of the object can be accessed using the functions term_to_tok, rule_to_tok and declaration_to_tok, respectively. These are the representations that would be used if the object were displayed by the Nuprl proof editor. This gives one a rudimentary way to check for defs.