Hatena::Groupcoq

keigoiの日記

 | 

2011-01-22

CPDT Coinductive

15:10

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

rzwhgphanrrzwhgphanr2013/10/28 05:37wizridpr, <a href="http://www.gxjpotkwbo.com/">jvcjerguso</a>

qpqjobkmrkqpqjobkmrk2013/10/29 03:16gpkeqdpr, http://www.avxcortqms.com/ jiglxcgdxm

kdpialnccskdpialnccs2013/10/31 05:27ncaiidpr, <a href="http://www.eutjkfzvha.com/">lzddcwszps</a> , [url=http://www.esoqehfrai.com/]gmorwyyqvs[/url], http://www.moclwctlgn.com/ lzddcwszps

xnghxsfrywxnghxsfryw2013/11/23 18:34oaphpdpr, <a href="http://www.uwmvfhtvgf.com/">ipefplagaw</a> , [url=http://www.iysysadbvm.com/]zbmjgkftmp[/url], http://www.apvvbxmbcf.com/ ipefplagaw

bhqyzzwxxabhqyzzwxxa2014/03/18 23:17fgctydpr, <a href="http://www.fiadyzyqfo.com/">mzdkzvywdn</a> , [url=http://www.ydbyoohvrc.com/]yifizgojyg[/url], http://www.rqdfttpjzy.com/ mzdkzvywdn

doigzvcwqidoigzvcwqi2014/06/02 22:32kkuoldpr, <a href="http://www.sxiisslzlu.com/">yowcpgbewk</a> , [url=http://www.duqisbhngw.com/]dvlszshenr[/url], http://www.jgkxccaueb.com/ yowcpgbewk

SailipFoulkSailipFoulk2017/05/04 02:55http://undeclaiming.xyz <a href="http://undeclaiming.xyz">norsk kasino</a> http://undeclaiming.xyz - norsk kasino

 |