The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/08/2014 06:52 PM, Saulo Araujo wrote:
> One more doubt. In the code below, the Coq compiler complains about the
> lines with Some value. It says "The constructor Some expects 1 argument.".
> When I change from Some value to Some v everything works fine. Is there
> something special about "Some value"?
>
> Fixpoint getValues objects name :=
>    match objects with
>      | object :: objects' =>
>        match getValue object name with
>          | Some value =>
>              match getValues objects' name with
>                | Some value' => Some (List.app value value')
>                | None => None
>              end
>          | None => None
>        end
>      | [] => Some []
>    end.

I would have to see the whole file prior to that definition to tell you 
what is going wrong.  The use of "value" in a binding position, such as 
in that match statement, shouldn't be a problem - but it might be the 
case that Coq isn't inferring the types the way you expect, depending on 
what comes before getValues.

-- Jonathan