// Generated by hobgoblin.