The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Hi Jonathan,
try replacing Qed with Defined. It should allow your function to evaluate.

Cheers,
Vincent

2011/12/20  
<jonathan.heras AT unirioja.es>:
> Dear all,
>
> I would like to know if it is possible to execute a recursive function which
> has been defined using the Function Command.
>
> For instance, if we have defined the following function (which merges two
> lists)
>
> Function merge2 (p:list Z*list Z)
> {measure (fun p=>(length (fst p))+(length (snd p)))} : list Z :=
> match p with
> | (nil,l) => l
> | (l,nil) => l
> | (x::xs,y::ys) => if Z_lt_ge_dec x y
> then x::(merge2 (xs,y::ys))
> else y::(merge2 (x::xs,ys))
> end.
> intros.
> simpl; auto with arith.
> intros.
> simpl; auto with arith.
> Qed.
>
> and now we are interested in computing
>
> Eval compute in merge2 ((1::3::5::nil),(2::4::6::nil)).
>
> In this case, the result that I obtain is
>
> let (v, _) :=
>           merge2_terminate
>             (1 :: 3 :: 5 :: Datatypes.nil, 2 :: 4 :: 6 :: Datatypes.nil) in
>       v
>     : list Z
>
> when I was expecting (1::2::3::4::5::6::nil).
>
> So, is it impossible to compute with a recursive function defined using
> Function?
>
> Thank you in advance.