coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?

From: Maxime Dénès <mail AT maximedenes.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?
Date: Thu, 18 Aug 2016 10:04:21 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT 12.mo5.mail-out.ovh.net
Ironport-phdr: 9a23:r8gvch2vdBMLBqNDsmDT+DRfVm0co7zxezQtwd8ZsegTL/ad9pjvdHbS+e9qxAeQG96KsrQe0KGP6fyoGTRZp83Q6DZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJLL+j4UrTfk96wn7jrvcaCOkMS33HkO+86bE3v616A7o9O2coqA51y4yOBmmFPdeVSyDEgDnOotDG42P2N+oV++T9bofMr+p0Ie6z7e6MlUe4QV2x+YChmrPHs4BLEVE6E4mYWemQQiBtBRQbfvz/gWZKklyLqt+9wkAUbO03tBeQxUDWmx6JiWB7thSsKMTMitm/N3J8jxJlHqQ6s8kQsi7XfZ5uYYaJz

Hi Hugo,

Do you have a pointer to this work?

Maxime.

On 08/17/16 23:53, Hugo Herbelin wrote:
> Note 2: Work was done recently by Meven Bertrand on how to use small
> inversion also in the inference of the inner return clauses of a
> nested pattern-matching problem. I hope this will eventually come into
> the code and increase further the strength of the pattern-matching
> algorithm.

Re: [Coq-Club] Proof irrelevance for equalities - is there a trick without axioms?, (continued)