[Agda] Classical Mathematics for a Constructive World

[Andreas Abel]

Nice slides, Peter!

Here are some remarks that came to me while reading your slides.
Cheers,
Andreas

slide 21

   It does not make much sense to define a Top-elimination rule.  In 
natural deduction, there is no such rule; it is an artifact of defining 
Top as a data type.  The definition as record

   record Top : P where

clearly does not give an elimination rule.  (I understand that you do 
not want to go into records in this tutorial, but maybe drop the 
Top-elim rule.)

slide 22

   If you start with conjunction and negation, should not be classical 
implication be defined as

    not (A and not B)

slide 34 3rd bullet

   n * 3 == n + n + n  needs induction on n, the wording on the slide is 
a bit misleading.  Simplification alone does not suffice.

On 17.12.12 2:53 PM, Peter Divianszky wrote:
> Hi,
>
> I have advertised Agda, I presented the attached slides for approx. 30
> mathematicians in Debrecen, Hungary, 20 of them were students.
> One of my students in Budapest translated the slides to English so I can
> present them to you.
>
> Your answers for my questions in this mailing list helped me a lot too,
> thank you very much.
>
> (I hope I didn't claim any false statement about Agda, please tell me if
> you find so.)
>
> Cheers,
> Peter
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
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/