[Agda] Positive numbers

[J.Burton at brighton.ac.uk]

At Tue, 3 Mar 2009 13:47:14 +0100,
Ulf Norell wrote:
>=20
> If you define the 0< predicate (called NonZero below) as a function retur=
ning 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 me=
ans that implicit arguments of type ⊤ can always
> be solved.
> Â=
> open import Data.Nat
> open import Data.Unit
> open import Data.Empty
>=20
> NonZero : ℕ → Set
> NonZero zero    =3D âŠ=
> NonZero (suc n) =3D âŠ=
>=20
> data Pos : Set where
> Â  pos : (n : â„•){p : NonZero n} -> Pos
>=20
> div : â„• -> Pos -> â„=
> div n (pos zero {()})
> div n (pos (suc m)) =3D {! !}
>=20
> test =3D div 5 (pos 3)
>=20
> Trying to give pos 0 : Pos will result in an unsolved implicit
> argument of type ⊥.

Thanks Ulf.

>=20
>     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?
>=20
> Salmon pink is the termination checkers way of telling you that it's not =
convinced that your function is terminating.
>=20

Ah, I see. Resisting the temptation to ask what yellow means led me to
find M-x customize-group agda2-highlight, which was illuminating.=20

Jim

> / Ulf
>=20
>=20