coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Yevgeniy Makarov" <emakarov AT gmail.com>
- To: judy AT mail.ccnu.edu.cn
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] question for help
- Date: Tue, 25 Sep 2007 17:58:25 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=JcWbGjTdFntRByYNmdF8k9XM4nnPoWzShiQ9vnktqZocdW6ZauU3zT+7dpbedYKrWg/QhWCCmP5i11gJz91p6kVnXgVPyJS3BG8hlYKpVLfj+Rg9RmArT8R4UVg6MZAdwAAZqkabiC4lMyW0J4JmoSoS/l94eYMV6UusUGd63yg=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
> Inductive tree (A:Type): Type :=
> tree_node : A -> forest A -> tree A
> with forest (A:Type):Type:=
> |nochild: forest A
> |addchild: tree A->forest A->forest A.
>
> 1 here what's A stands for? means the node's type is Type? can I change
> Type to
> nat?
A is the type of things that are stored in the tree, i.e., the type of
tree labels. A itself has sort Type, which means that A can be
basically any type (nat, list, ~ A /\ B, etc.).
> 2 how to present in a tree T, node1 is the father of node 2 ,node 3..,or
> node2
> is
> the son of the only father node 1.
Here is an example of a tree:
Definition t := tree_node nat 0 (addchild nat (tree_node nat 1
(nochild nat)) (nochild nat)).
The type of the labels (A above) is nat. The tree has two nodes: one
has label 0, its son has label 1.
This seems a little verbose, so in the beginning (before declaring
tree) you can say
Set Implicit Arguments.
and then after defining tree
Implicit Arguments nochild [A].
Then the same example can be written as
Definition t := tree_node 0 (addchild (tree_node 1 nochild) nochild).
> 3 how to define direction graph structure? and how to present in a graph
> G,and
> how
> to define the relation between faher and son.
Data in Coq is represented using inductive types. You can read a
tutorial on inductive types on the Coq documentation web page.
Yevgeniy
- [Coq-Club] question for help,
- Re: [Coq-Club] question for help, Yevgeniy Makarov
Archive powered by MhonArc 2.6.16.