The Coq mailing list

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

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