The Coq mailing list

[roconnor AT theorem.ca]

On Fri, 16 Oct 2009, AUGER Cédric wrote:

> (*-- It is fundamental, but as you did below, we can have dependent types,
> which accepts different parameters,
> and dealing is not as easy as with non dependent types *)

It appears Agda can do it, so I don't understand why you say it is 
fundamental.

module SillyTree where
{- my first agda program -}
data bool : Set where
  true : bool
  false : bool

mutual
  data SillyTree : bool -> Set where
    leaf : SillyTree true
    node : (b : bool) -> SillyTreePair b -> SillyTree false

  data SillyTreePair (b : bool) : Set where
    stp : SillyTree b -> SillyTree b -> SillyTreePair b

sillyFunction : SillyTree false -> bool
sillyFunction (node true (stp leaf leaf)) = true
sillyFunction _ = false

> (*-- And what about: *)
> Inductive SillyTree : bool -> Type :=
> | leaf : SillyTree true
> | node : SillyTreePair -> SillyTree false
> with SillyTreePair : Type :=
> | stp : forall b, SillyTree b -> SillyTree b -> SillyTreePair.

This is nice, but not adequate for my purposes because I want to have 
SillyTreePair indexed by bool for the other uses of SillyTreePair I have 
in mind.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''