-
- \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.