Expressions whose sizes and types are sensible.
We say expressions are well-typed when their signs and widths have been computed, and when certain consistency requirements are met. This is a rather elaborate consistency check we use as a basic correctness property of our expression-sizing transformation. It may also be useful in later transformations to insist that the you are working with reasonably sane expressions.
Every atom in the expression must satisfy vl-atom-welltyped-p.
Every nonatom has certain consistency checks that depend upon which operator
is being applied. For instance, in an expression like