I always thought the statement

    {-# BUILTIN NATURAL ℕ #-}

binds the inductive definition of ℕ to an efficient implementation. However, googling now I can find no confirmation of this. Does anyone know more?