The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Fully expecting someone on the list to respond chastising me for giving 
an "unhelpful" answer: Have you read CPDT 
<http://adam.chlipala.net/cpdt/>, or specifically the first few chapters 
in the part on dependent types?  There are a number of design patterns 
for doing the sort of thing you're trying to do, and I think it is more 
useful to read a general introduction than to read ad-hoc answers on 
this mailing list.

On 07/02/2013 05:28 PM, Ilmārs Cīrulis wrote:
> Fixpoint example (m n:nat) (p: m<=n): list nat :=
> match m with
> | O => nil
> | S m' => cons m (example m' n (ttt m' n p))
> end.
>
>
> It gives similar error as before:
>
> Error:
> In environment
> example : forall m n : nat, m <= n -> list nat
> m : nat
> n : nat
> p : m <= n
> m' : nat
> The term "p" has type "m <= n" while it is expected to have type "S m' 
> <= n".
>
>
> So I suppose that I didn't keep the link between <m> and <m'> good 
> enough. Any ideas how to do it?