The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

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