The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

 > My name is Joao
 > I'm a new member of the Coq Club.
 > I would like to know how to define new operations using the
 > recursive scheme _rec
 > I. e. If I have the next definition:
 > Coq < Inductive list [X:Set]:Set :=
 > Coq < Nil : (list X)
 > Coq < | Cons: X -> (list X) -> (list X).
 > list_ind is defined
 > list_rec is defined
 > list_rect is defined
 > list is defined
 > 
 > How I could define a function that concatenate two lists using
 > list_rec?

Such   lists  already   exist  in   the  Coq   standard   library,  in
Lists/PolyList.v. In particular, concatenation is defined, like this:

======================================================================
Fixpoint app [l:list] : list -> list 
      := [m:list]Cases l of
                   nil         => m 
                 | (cons a l1) => (cons a (app l1 m))
                 end.
======================================================================

Hope this helps,
-- 
Jean-Christophe Filliatre (http://www.lri.fr/~filliatr)