coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Saulo Araujo <saulo2 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Beginner Question
- Date: Sat, 8 Nov 2014 22:51:30 -0300
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
- [Coq-Club] Beginner Question, saulo2, 11/08/2014
- Re: [Coq-Club] Beginner Question, Jonathan, 11/08/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/08/2014
- Re: [Coq-Club] Beginner Question, Jonathan, 11/08/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/08/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/09/2014
- Re: [Coq-Club] Beginner Question, Jonathan, 11/09/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/09/2014
- Re: [Coq-Club] Beginner Question, Jonathan, 11/09/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/09/2014
- Re: [Coq-Club] Beginner Question, Pierre Casteran, 11/09/2014
- Re: [Coq-Club] Beginner Question, Jonathan, 11/09/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/09/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/08/2014
- Re: [Coq-Club] Beginner Question, Jonathan, 11/08/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/08/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/08/2014
- Re: [Coq-Club] Beginner Question, Jonathan, 11/08/2014
Archive powered by MHonArc 2.6.18.