The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

> This *is* your definition.
> 
> In other words:
> 
> Definition take (A : Type) (n : nat) (s : LList A) := match n, l with
> | 0, _ => LNil | S n', LCons a l' => LCons a (take n' l') end.
> 
> Definition inductively_defined (A B : Type) (P : LList A -> B) :=
>     forall s, P s -> exists n, forall n', n <= n' -> P (take n' s).

Thank you for enlightening me. 
It is always difficult to know what is the definition and what are derived 
facts.

This raised another question to me: 

If any predicate on LList can be somehow constructed
from inductively_defined ones and its negations (i.e. predicates which do not 
hold
for finite lists), possibly in the presence or absence of the excluded middle.

Maybe it can be rephrased as: 

What would be a nice algebra/combinators on predicates over LList?

It would be also great if you could give me any reference; 
meanwhile I should dig into Peter's mail. 

Kind regards,
Keiko