Prove basic properties about a matching function.
Note: typically, you should only want to use this macro if you are defining a new matching function. If you are just using existing matching functions like sin-match-lit to write your own lexer, this isn't what you want.
Form: (def-match-thms name)
This expands into a make-event. The
Well-Typed. The match is either a non-empty string or nil. Note that
there is generally no reason to prove anything about the well-formedness of
Progress. The length of the input stream's contents never increases, and always decreases when text is matched.
Reconstruction. Appending the matched text onto the new input stream's contents yields the original input stream's contents. In other words, the matcher properly matches text from the front of the stream.
Graceful Failure. If there is no match, the stream is unchanged.
Match-Free Failure. (weak matchers only) If the weak matcher
fails (i.e., it signals that