The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi Guillaume,

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.
==================================

Cheers,

--
gallais



On 21 February 2012 21:07, Guillaume Yziquel
<guillaume.yziquel AT citycable.ch>
 wrote:
> Hi. Got a newbie question:
>
> How do you deal with 'subtyping' when using the { .. | .. } notation?
> Typically, how would one deal with this situation?
>
>        Coq < Definition pos := {n : nat | n >= 1}.
>        pos is defined
>
>        Coq < Definition suc (n : pos) := S n.
>        Toplevel input, characters 30-31:
>        > Definition suc (n : pos) := S n.
>        >                               ^
>        Error: In environment
>        n : pos
>        The term "n" has type "pos" while it is expected to have type
>        "nat".
>
> --
>     Guillaume Yziquel