[Agda] Positive numbers

[Ulf Norell]

On Tue, Mar 3, 2009 at 12:39 AM, Jim Burton <jim at sdf-eu.org> wrote:

> So I have to make values of N+ with (pos n is-succ). I would like the
> is-succ argument to be implicit, as it must be redundant, but doing
> that allows (pos zero). How can I fix that?


If you define the 0< predicate (called NonZero below) as a function
returning either the empty type or the singleton type instead of inductively
you can leave the proof implicit. The reason is that we have eta equality on
the singleton type (any object x : ⊤ is equal to the unique element of ⊤),
which means that implicit arguments of type ⊤ can always be solved.

open import Data.Nat
open import Data.Unit
open import Data.Empty

NonZero : ℕ → Set
NonZero zero    = ⊥
NonZero (suc n) = ⊤

data Pos : Set where
  pos : (n : ℕ){p : NonZero n} -> Pos

div : ℕ -> Pos -> ℕ
div n (pos zero {()})
div n (pos (suc m)) = {! !}

test = div 5 (pos 3)

Trying to give pos 0 : Pos will result in an unsolved implicit argument of
type ⊥.

Incidentally, emacs highlights _div_ and  div in the above in salmon pink
> whereas other functions are in dark blue -- is there something special
> about it?


Salmon pink is the termination checkers way of telling you that it's not
convinced that your function is terminating.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090303/3d93ba5b/attachment.html