The value of a cast is the value of its body, unchanged. The type of this
value is equal to the target type, not the type of its body.
-
- \todo{Move and update this paragraph}
- Note that this syntax is also used sometimes to indicate that a particular
- expression has a particular type, even when no cast expression is
- involved. This is then purely informational, since the only elements that
- are explicitly typed in the Core language are the binder references and
- cast expressions, the types of all other elements are determined at
- runtime.
\stopdesc
\startdesc{Note}