Expository math is content in a Lurch document that is meant to be read for human comprehension but not as part of the logical content of a proof. For instance, a document author might want to add some side comments that include variables, equations, or other expressions, typeset with LaTeX, but that are not intended for the system to grade, interpret, or obey.

For example, if an instructor is writing the rules for a logical system, they might want to show how NOT to use the rules, or how NOT to write expressions, and they don't want their document to contain validation errors, as if there were something wrong with it, when it's really just showing by example what to avoid.

We therefore provide a new type of Atom that functions very similar to the Expression type, with two exceptions. First, the notation used is LaTeX, not Lurch notation. Second, the content is not interpreted by the system for use in validation; more precisely, it is completely ignored during the conversion of a document to LCs, which is then used in validation.