The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Greetings,

Is exists some practical article about Function command?
I need this feature but I have problems all the time and I don't
understand why. (I used this function for creating recursive functions
under type "list (list my_inductive_type)".
For example, why this function with proof below is blocking when I call it:

Definition padajuca_funkcija (x : nat) : nat := 6-x.

Function dd_k (xkc ykc : nat) {measure padajuca_funkcija xkc} : Prop :=
if le_lt_dec xkc 5 then
  if le_lt_dec ykc 5 then
    if eq_figure (nth (ykc+1) (nth (xkc+1) lista nil) v) D then True
    else
      if eq_figure (nth (ykc+1) (nth (xkc+1) lista nil) v) L then True
      else
        if eq_figure (nth (ykc+1) (nth (xkc+1) lista nil) v) O then dd_k
(S xkc) (S ykc)
        else False
  else False
else False.

intros.
unfold padajuca_funkcija.
destruct (le_lt_dec xkc 5).
omega.
absurd (v=O).
discriminate.
rewrite <- anonymous3.
rewrite nth_overflow;auto.
rewrite nth_overflow;[simpl;omega|rewrite H_lista;simpl;omega].
Defined.

Thanks for advice,

Marko Malikoviæ