The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

Did you expected something like this:

Inductive sortedlist : nat -> Set :=
   | snil : forall n, sortedlist n
   | scons : forall (n n':nat) (l:sortedlist n'), n <= n' -> sortedlist n.

?

I am not sure why it didn't worked, so i won't try to explain it...

Btw, you also ill-typed the rest of your term:
leq_all' -> leq_all
leq_all n nil -> leq_all n snil
leq_all n (cons n' l') -> leq_all n (scons n' l')

> I was trying to reproduce an example similar to one from the Agda
> documentation, using dependent types to define the type of a sorted
> list of numbers:
>
> Inductive sortedlist : Set :=
>    | snil : sortedlist
>    | scons : forall (n:nat) (l:sortedlist), leq_all' n l -> sortedlist
> with leq_all : nat -> sortedlist -> Prop :=
>    | srt_nil : forall n, leq_all n nil
>    | srt_cons : forall n n' l', n <= n' -> leq_all n l' -> leq_all n
> (cons n' l')
> .
>
> but it gives an error on "sortedlist" in the type of leq_all:
>      leq_all : nat -> sortedlist -> Prop :=
> "Error: The reference sortedlist was not found in the current
> environment."
>
> Apparently, the names of the types being defined cannot be used in the
> types of other mutually referential definitions? Is there any way to
> do this?
>
> --- nadeem
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>


-- 
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay