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 _∸_

Page last modified on June 14, 2007, at 01:35 PM

Powered by
PmWiki