The Coq mailing list

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

Hi Saulo,

 The symbol "value" is  already defined as a synonymous for "Some"  
(in the file theory/Init/Specif.v)

Coq < Print value.
value = Some
     : forall A : Type, A -> option A

Argument A is implicit
Argument scopes are [type_scope _]

Coq < Locate value.
Constant Coq.Init.Specif.value


It seems that Coq (8.4pl4)  doesn't like the use of  names of  
constructors as pattern variables.

Compute match (cons 3 nil) with nil => 67 | cons S tl => S end.
                                                  ^
Error: The constructor S expects 1 argument.


Notice that using names that are  bound to non-constructors seems to be OK.

Coq < Definition foo := plus.
foo is defined

Coq < Compute match 56 with 0 => 6 | S foo => foo end.
Warning: pattern foo is understood as a pattern variable
     = 55
     : nat


Best regards,

Pierre








Quoting Saulo Araujo 
<saulo2 AT gmail.com>:

> Hi Jonathan,
>
> I am sending the whole file but, since changing from Some value to Some v
> did the tricky, don't bother trying to understand what is happening unless
> you are curious ;)
>
> Require Import String.
> Open Scope string_scope.
>
> Require Import List.
> Import ListNotations.
>
> Definition compareStrings x y :=
>   if string_dec x y then true else false.
>
> Inductive CLASS : Type :=
>   Class : string -> list (string * string) -> CLASS.
>
> Definition getClass classes id :=
>   List.find
>   (fun class => let 'Class id' _ := class in compareStrings id' id)
>   classes.
>
> Inductive OBJECT : Type :=
>   Object : string -> string -> list (string * list string) -> OBJECT.
>
> Definition getObject objects id :=
>   List.find
>   (fun object => let 'Object id' _ _ := object in compareStrings id' id)
>   objects.
>
> Definition getAttribute attributes name :=
>   List.find
>   (fun attribute : string * list string =>
>      let (name', _) := attribute in compareStrings name' name)
>   attributes.
>
> Definition getValue object name :=
>   let 'Object _ _ attributes := object in
>     match getAttribute attributes name with
>       | Some attribute => let (_, value) := attribute in Some value
>       | None => None
>     end.
>
> 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.
>
> Thanks again!
> Saulo
>
> On Sat, Nov 8, 2014 at 9:34 PM, Jonathan 
> <jonikelee AT gmail.com>
>  wrote:
>
> > 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