Inhabited and Uninhabited Types

Model logic using the empty enum type to denote unreachable code paths.