The Coq mailing list

[Guillaume Yziquel <guillaume.yziquel AT citycable.ch>]

Le Tuesday 21 Feb 2012 à 21:23:34 (+0000), gallais @ ensl.org a écrit :
> Hi Guillaume,

Hi.

> Have you tried declaring a coercion ?
> 
> ==================================
> Definition pos := {n : nat | n >= 1}.
> Definition posnat (p : pos) : nat := proj1_sig p.
> 
> Coercion posnat : pos >-> nat.
> 
> Definition suc (n : pos) := S n.
> ==================================

No, I did not now about Coercion. Quite nice.

In fact, I just noticed the following link

        http://adam.chlipala.net/cpdt/html/Subset.html

and the following code fragment within:

        Definition pred_strong2 (s : {n : nat | n > 0}) : nat :=
          match s with
            | exist O pf => match zgtz pf with end
            | exist (S n') _ => n'
          end.

which gives me a clearer understanding of how to deconstruct inhabitants
of the {n : nat | n > 0} type.

Thanks for your quick and helpful answer.

-- 
     Guillaume Yziquel