Filtering...

abbrevs

books/std/strings/abbrevs

Included Books

top
other
(in-package "ACL2")
include-book
(include-book "top")
catmacro
(defmacro cat (&rest args) `(cat . ,ARGS))
append-charsmacro
(defmacro append-chars (x y) `(append-chars ,X ,Y))
other
(add-macro-alias append-chars append-chars)
append-firstn-charsmacro
(defmacro append-firstn-chars
  (n x y)
  `(append-firstn-chars ,N ,X ,Y))
other
(add-macro-alias append-firstn-chars
  append-firstn-chars)
revappend-charsmacro
(defmacro revappend-chars
  (x y)
  `(revappend-chars ,X ,Y))
other
(add-macro-alias revappend-chars revappend-chars)
charlisteqvmacro
(defmacro charlisteqv (x y) `(charlisteqv ,X ,Y))
other
(add-macro-alias charlisteqv charlisteqv)
collect-strs-with-isubstrmacro
(defmacro collect-strs-with-isubstr
  (a x)
  `(collect-strs-with-isubstr ,A ,X))
other
(add-macro-alias collect-strs-with-isubstr
  collect-strs-with-isubstr)
collect-syms-with-isubstrmacro
(defmacro collect-syms-with-isubstr
  (a x)
  `(collect-syms-with-isubstr ,A ,X))
other
(add-macro-alias collect-syms-with-isubstr
  collect-syms-with-isubstr)
dec-digit-char-pmacro
(defmacro dec-digit-char-p (x) `(dec-digit-char-p ,X))
other
(add-macro-alias dec-digit-char-p dec-digit-char-p)
dec-digit-char-valuemacro
(defmacro dec-digit-char-value
  (x)
  `(dec-digit-char-value ,X))
other
(add-macro-alias dec-digit-char-value
  dec-digit-char-value)
dec-digit-char-list*pmacro
(defmacro dec-digit-char-list*p
  (x)
  `(dec-digit-char-list*p ,X))
other
(add-macro-alias dec-digit-char-list*p
  dec-digit-char-list*p)
dec-digit-char-list-valuemacro
(defmacro dec-digit-char-list-value
  (x)
  `(dec-digit-char-list-value ,X))
other
(add-macro-alias dec-digit-char-list-value
  dec-digit-char-list-value)
charlistnat<macro
(defmacro charlistnat< (x y) `(charlistnat< ,X ,Y))
other
(add-macro-alias charlistnat< charlistnat<)
firstn-charsmacro
(defmacro firstn-chars (x y) `(firstn-chars ,X ,Y))
other
(add-macro-alias firstn-chars firstn-chars)
html-encode-stringmacro
(defmacro html-encode-string
  (x tabsize)
  `(html-encode-string ,X ,TABSIZE))
other
(add-macro-alias html-encode-string html-encode-string)
ichareqvmacro
(defmacro ichareqv (x) `(ichareqv ,X))
other
(add-macro-alias ichareqv ichareqv)
ichar<macro
(defmacro ichar< (x y) `(ichar< ,X ,Y))
other
(add-macro-alias ichar< ichar<)
icharlisteqvmacro
(defmacro icharlisteqv (x) `(icharlisteqv ,X))
other
(add-macro-alias icharlisteqv icharlisteqv)
icharlist<macro
(defmacro icharlist< (x y) `(icharlist< ,X ,Y))
other
(add-macro-alias icharlist< icharlist<)
iprefixpmacro
(defmacro iprefixp (x) `(iprefixp ,X))
other
(add-macro-alias iprefixp iprefixp)
istreqvmacro
(defmacro istreqv (x) `(istreqv ,X))
other
(add-macro-alias istreqv istreqv)
istr<macro
(defmacro istr< (x y) `(istr< ,X ,Y))
other
(add-macro-alias istr< istr<)
istrsortmacro
(defmacro istrsort (x) `(istr-sort ,X))
other
(add-macro-alias istrsort istr-sort)
istrposmacro
(defmacro istrpos (x y) `(istrpos ,X ,Y))
other
(add-macro-alias istrpos istrpos)
istrprefixpmacro
(defmacro istrprefixp (x y) `(istrprefixp ,X ,Y))
other
(add-macro-alias istrprefixp istrprefixp)
isubstrpmacro
(defmacro isubstrp (x y) `(isubstrp ,X ,Y))
other
(add-macro-alias isubstrp isubstrp)
prefix-linesmacro
(defmacro prefix-lines
  (x prefix)
  `(prefix-lines ,X ,PREFIX))
other
(add-macro-alias prefix-lines prefix-lines)
rpadcharsmacro
(defmacro rpadchars (x len) `(rpadchars ,X ,LEN))
other
(add-macro-alias rpadchars rpadchars)
rpadstrmacro
(defmacro rpadstr (x len) `(rpadstr ,X ,LEN))
other
(add-macro-alias rpadstr rpadstr)
lpadcharsmacro
(defmacro lpadchars (x len) `(lpadchars ,X ,LEN))
other
(add-macro-alias lpadchars lpadchars)
lpadstrmacro
(defmacro lpadstr (x len) `(lpadstr ,X ,LEN))
other
(add-macro-alias lpadstr lpadstr)
strsplitmacro
(defmacro strsplit (x del) `(strsplit ,X ,DEL))
other
(add-macro-alias strsplit strsplit)
strposmacro
(defmacro strpos (x y) `(strpos ,X ,Y))
other
(add-macro-alias strpos strpos)
strrposmacro
(defmacro strrpos (x y) `(strrpos ,X ,Y))
other
(add-macro-alias strrpos strrpos)
strsubstmacro
(defmacro strsubst (x y z) `(strsubst ,X ,Y ,Z))
other
(add-macro-alias strsubst strsubst)
strprefixpmacro
(defmacro strprefixp (x y) `(strprefixp ,X ,Y))
other
(add-macro-alias strprefixp strprefixp)
strsuffixpmacro
(defmacro strsuffixp (x y) `(strsuffixp ,X ,Y))
other
(add-macro-alias strsuffixp strsuffixp)
substrpmacro
(defmacro substrp (x y) `(substrp ,X ,Y))
other
(add-macro-alias substrp substrp)
strnat<macro
(defmacro strnat< (x y) `(strnat< ,X ,Y))
other
(add-macro-alias strnat< strnat<)
strtokmacro
(defmacro strtok (x y) `(strtok ,X ,Y))
other
(add-macro-alias strtok strtok)
strvalmacro
(defmacro strval (x) `(strval ,X))
other
(add-macro-alias strval strval)
strval8macro
(defmacro strval8 (x) `(strval8 ,X))
other
(add-macro-alias strval8 strval8)
strval16macro
(defmacro strval16 (x) `(strval16 ,X))
other
(add-macro-alias strval16 strval16)