The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

I feel like I might still not understand exactly what is needed, but perhaps
this is a solution?

Inductive SillyTreePair SillyTree (b:bool) : Type :=
| stp : SillyTree b -> SillyTree b -> SillyTreePair SillyTree b.

Inductive SillyTree : bool -> Type :=
| leaf : SillyTree true
| node : forall b, SillyTreePair SillyTree b -> SillyTree false.

Definition sillyFunction (st:SillyTree false) : bool :=
  match st with
    | node a (stp leaf leaf) => a
    | _ => false
  end.

SillyTree is making use of the fact that SillyTreePair f b is a strictly
positive operator in f.

-- 
View this message in context: 
http://www.nabble.com/Parametricity-in-Mutual-Inductive-Types-tp25930552p25937693.html
Sent from the Coq mailing list archive at Nabble.com.