Def-prefix/remainder-thms
Introduce prefix/remainder theorems for a lexing function.
Many of our lexing routines take echars, an vl-echarlist-p, as input, and split this list into a prefix and
remainder. This macro allows us to quickly prove several common
properties about such a function. In particular, we show:
- prefix is always a true-listp, and furthermore it is also a
vl-echarlist-p as long as the echars is.
- remainder is a true-listp exactly when echars is, and furthermore
it is a vl-echarlist-p whenever echars is.
- Appending the prefix and remainder always returns the original
echars. A corollary is that whenever prefix is empty, remainder
is the whole of echars.
- The acl2-count of remainder is never greater than that of echars,
and strictly decreases whenever prefix is non-nil.
Subtopics
- Vl-read-string-escape-sequence-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-string-escape-sequence,
automatically generated by def-prefix/remainder-thms.
- Vl-read-non-zero-unsigned-number-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-non-zero-unsigned-number,
automatically generated by def-prefix/remainder-thms.
- Vl-read-through-literal-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-through-literal,
automatically generated by def-prefix/remainder-thms.
- Vl-read-until-literal-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-until-literal,
automatically generated by def-prefix/remainder-thms.
- Vl-read-some-literal-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-some-literal,
automatically generated by def-prefix/remainder-thms.
- Vl-read-simple-identifier-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-simple-identifier,
automatically generated by def-prefix/remainder-thms.
- Vl-read-octal-string-escape-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-octal-string-escape,
automatically generated by def-prefix/remainder-thms.
- Vl-read-hex-string-escape-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-hex-string-escape,
automatically generated by def-prefix/remainder-thms.
- Vl-read-escaped-identifier-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-escaped-identifier,
automatically generated by def-prefix/remainder-thms.
- Vl-read-unsigned-number-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-unsigned-number,
automatically generated by def-prefix/remainder-thms.
- Vl-read-decimal-value-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-decimal-value,
automatically generated by def-prefix/remainder-thms.
- Vl-read-octal-value-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-octal-value,
automatically generated by def-prefix/remainder-thms.
- Vl-read-decimal-base-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-decimal-base,
automatically generated by def-prefix/remainder-thms.
- Vl-read-binary-value-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-binary-value,
automatically generated by def-prefix/remainder-thms.
- Vl-read-binary-base-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-binary-base,
automatically generated by def-prefix/remainder-thms.
- Vl-read-time-unit-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-time-unit,
automatically generated by def-prefix/remainder-thms.
- Vl-read-string-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-string,
automatically generated by def-prefix/remainder-thms.
- Vl-read-real-tail-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-real-tail,
automatically generated by def-prefix/remainder-thms.
- Vl-read-octal-base-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-octal-base,
automatically generated by def-prefix/remainder-thms.
- Vl-read-literal-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-literal,
automatically generated by def-prefix/remainder-thms.
- Vl-read-include-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-include,
automatically generated by def-prefix/remainder-thms.
- Vl-read-hex-value-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-hex-value,
automatically generated by def-prefix/remainder-thms.
- Vl-read-hex-base-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-hex-base,
automatically generated by def-prefix/remainder-thms.
- Vl-read-any-base-prefix/remainder-thms
- Prefix and remainder theorems for vl-read-any-base,
automatically generated by def-prefix/remainder-thms.
