<div dir="ltr">If you're interested in Ramsey's theorem for the purpose of termination I suggest you read the paper "Stop When You Are Almost-Full", by Dimitrios Vytiniotis, Thierry Coquand and David Wahlstedt. They develop an intuitionistic Ramsey theorem to be used for proving termination. The paper uses Coq but there is an Agda formalization here:<div>
<a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.IntuitionisticRamseyTheorem">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.IntuitionisticRamseyTheorem</a></div><div><br></div><div>Josef<br><div><br>
</div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jul 4, 2014 at 1:29 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">People,<br>
<br>
is there publicly available a proof in Agda of the Ramsey's theorem<br>
(about the size of a monochromatic sub-graph in a complete graph)<br>
?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>