coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to prove functions are equal?

From: Robin Green <greenrd AT greenrd.org>
To: Conor McBride <conor AT strictlypositive.org>
Cc: Coq Club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] How to prove functions are equal?
Date: Mon, 2 Jun 2008 15:24:20 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: Swansea University

On Mon, 2 Jun 2008 15:07:24 +0100
Conor McBride
<conor AT strictlypositive.org>
wrote:

> PS In the last few days, I've managed to
> construct the extensional universe from
> "Observational Equality, Now!" (Altenkirch,
> McBride, Swierstra, 2007) in Coq. By
> reflecting on this universe, one can build
> an equality which is extensional and
> substitutive, whilst retaining canonicity
> for datatypes.

I'd be interested in using this. Is a public release expected soon?
--
Robin

[Coq-Club] How to prove functions are equal?, Wan Hai
- Re: [Coq-Club] How to prove functions are equal?, Adam Chlipala
  - Re: [Coq-Club] How to prove functions are equal?, Bruno Barras
- Re: [Coq-Club] How to prove functions are equal?, Florian Hatat
  - Re: [Coq-Club] How to prove functions are equal?, Wan Hai
  - Re: [Coq-Club] How to prove functions are equal?, Conor McBride
    - Re: [Coq-Club] How to prove functions are equal?, Robin Green
      - Re: [Coq-Club] How to prove functions are equal?, Conor McBride
    - Re: [Coq-Club] How to prove functions are equal?, Thorsten Altenkirch