The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Envy:  My coq installation does not have the proof-theoretical power of 
yours...

Or how did you define S?

Cheers,
Andreas

On 9/21/11 2:17 PM, Andrej Bauer wrote:
> It was Thorsten Altenkirch's birthday yesterday. I thought it would be
> appropriate to show him how Coq can also do all those things that Agda
> does. Enjoy:
>
> http://vimeo.com/29361996
>
> With kind regards,
>
> Andrej

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/