[Agda] Re: [Coq-Club] Propositional extensionality: the return of the revenge

[Andreas Abel]

On 03.03.2014 09:37, Altenkirch Thorsten wrote:
> On 02/03/2014 19:07, "Andreas Abel" <abela at chalmers.se> wrote:
>> This concerns the current "musical" coinduction mechanism (which was
>> never sound anyway).
>
> Musical = flat and sharp. Why is this not sound?

Haha! :)

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

Depeartment of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/