Exercises of http://adam.chlipala.net/cpdt/html/Coinductive.html
(* Define a co-inductive type of infinite trees carrying data of a fixed parameter type. Each node should contain a data value and two child trees. *) Section Inf_tree. Variable A : Set. CoInductive my_inf_tree : Set := | Node : A -> my_inf_tree -> my_inf_tree -> my_inf_tree. End Inf_tree. (* Define a function everywhere for building a tree with the same data value at every node. *) CoFixpoint everywhere (A:Set) (x:A) : my_inf_tree A := Node A x (everywhere A x) (everywhere A x).