coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Andreas Abel <abela AT chalmers.se>
To: Altenkirch Thorsten <psztxa AT exmail.nottingham.ac.uk>, "coq-club AT inria.fr" <coq-club AT inria.fr>, Agda List <agda AT lists.chalmers.se>
Subject: Re: [Coq-Club] [Agda] Re: Propositional extensionality: the return of the revenge
Date: Mon, 3 Mar 2014 09:46:52 +0100

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/

Re: [Coq-Club] Propositional extensionality: the return of the revenge, Andreas Abel, 03/02/2014
- Re: [Coq-Club] [Agda] Re: Propositional extensionality: the return of the revenge, Maxime Dénès, 03/02/2014
- Re: [Coq-Club] [Agda] Re: Propositional extensionality: the return of the revenge, Altenkirch Thorsten, 03/03/2014
  - Re: [Coq-Club] [Agda] Re: Propositional extensionality: the return of the revenge, Andreas Abel, 03/03/2014