20070614-3

I want to define natural number subtraction as follows:

 module Bug where

 data ℕ : Set where
   zero : ℕ
   suc  : ℕ -> ℕ

 {-# BUILTIN NATURAL ℕ    #-}
 {-# BUILTIN ZERO    zero #-}
 {-# BUILTIN SUC     suc  #-}

 _∸_ : ℕ -> ℕ -> ℕ
 m     ∸ zero  = m
 zero  ∸ suc n = zero
 suc m ∸ suc n = m ∸ n

 {-# BUILTIN NATMINUS _∸_ #-}

However, this is not accepted by the BUILTIN pragma:

 zero ∸ m != zero of type ℕ
 when checking the pragma BUILTIN NATMINUS _∸_