The Coq mailing list

[David Pichardie <david.pichardie AT irisa.fr>]

Dear Adam,

You have effectively a syntax problem:

>    Fixpoint Computable (M: Term) {measure M term_type_measure} : Prop 
> :=
>    match (type M) with
>    | #T => AccR M
>    | TL --> TR =>
>        forall P (Papp: isApp P) (PL: appBodyL Papp = M) (typeL: type P 
> = TR),
>      Computable (appBodyR Papp) ->
>      Computable P
>    end.
>   

should be

>  Function Computable (M: Term) {measure term_type_measure M} : Prop :=
>   match (type M) with
>   | #T => AccR M
>   | TL --> TR =>
>       forall P (Papp: isApp P) (PL: appBodyL Papp = M) (typeL: type P 
> = TR),
>     Computable (appBodyR Papp) ->
>     Computable P
>   end.

Unfortunately, you will now obtain a Coq error like "User error: 
find_call_occs : Prod".

I am not expert in the current implementation of Function but I think 
you are too greedy for us.
Your quantification "forall P Papp" before the recursive call is too 
difficult for the current capabilities of Function.

Sorry,  I think you will have to present you problem in a different way 
if you want to use Function here.

Best,

David.