The Coq mailing list

["" <judy AT mail.ccnu.edu.cn>]

HI:

I found in some referrence a way to define stucture Tree :

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?
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.
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.


yours Judy