Lines Matching refs:str
96 val _ = declare_names ("ACL2_STRING", "str");
159 `(stringp(str x) = t) /\ (stringp _ = nil)`;
680 (sexp_size (str a) = 1) /\
728 `(coerce (str s) y =
731 else str "")
736 else str(coerce_list_to_string(make_character_list(cons a x))))
738 (coerce _ y = if y = sym "COMMON-LISP" "LIST" then nil else str "")`;
1152 `(symbol_name (sym p n) = ite (symbolp (sym p n)) (str n) (str ""))
1154 (symbol_name _ = (str ""))`;
1168 ite (symbolp (sym p n)) (str p) (str ""))
1170 (symbol_package_name _ = (str ""))`;
1205 `(pkg_witness (str x) =
1213 `(pkg_witness (str x) =
1214 ite (equal (str x) (str ""))
1239 `(intern_in_package_of_symbol (str x) (sym p n) =