The Coq mailing list

["agnes gonnet" <agnesgon AT hotmail.com>]

Hi,

could anyone explain me what is wrong with the following mutually recursive 
functions :


Inductive operation : Set :=
|OP2pt : operation
|OPany : operation.

Inductive exp : Set :=
|Espace : exp
|Emot : nat -> exp
|Eop : operation -> list exp -> exp.

Parameter env_extern : list nat.
Parameter list_exp : list exp.
Parameter Et : exp -> exp -> exp.
Parameter in_bool: (nat -> nat -> bool) -> nat -> list nat -> bool.


Fixpoint eval_exp  (e:exp) {struct e}: option exp  :=
match e with
 | Espace => Some Espace
 | Emot id => Some (Emot id)
 | Eop OP2pt (e1::e2::nil) =>
     match (eval_exp e1) with
     |Some(Emot id1) => match (eval_exp e2) with
                |Some (Emot id2) => if in_bool beq_nat id2 env_extern
                          then Some Espace
                          else None
        |_ => None
        end
      |_ => None
      end

 |Eop Opany (e1::e2::nil) =>  eval_op list_exp e2
 |_ => None
end
with eval_op  (l:list exp) (e:exp) {struct l} : option exp :=
  match l with
  |nil => Some (Espace)
  |e1::l1 => match (eval_exp (Eop OP2pt (e1::e::nil))) with
        |Some res => match (eval_op l1 e) with
                   |Some res1 => Some (Et res res1)
                   |None => None
                   end
        |None => None
        end
   end.


Thanks.