## type-binding rule - The type-binding rule states that terms are explicitly typed whenever this is allowed by the Lean syntax rules. - We are trading extra wordiness for the clarity of having the term and the type being as close together as possible. ## Examples ![[exact-show#exact-show]]