The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi, agnes,

I have some problems in understanding your example.
In particular, the role played by the parameter list_exp in the 
recursive call
to eval_op. It is not one of the constituents given by the 
destructuration of e
(the names of which are given in the error message).

Could you specify informally what should compute eval_exp and eval_op ?
Pierre






agnes gonnet wrote:

> 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.
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club