coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about Extraction

From: "John Wiegley" <johnw AT newartisans.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Question about Extraction
Date: Mon, 07 Sep 2015 14:57:13 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pa0-f43.google.com
Ironport-phdr: 9a23:TSh4mxZd1pcIYdpnx6I+ikz/LSx+4OfEezUN459isYplN5qZpci7bnLW6fgltlLVR4KTs6sC0LqK9fm4EjVevN6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDuvcSLKFwW2XKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzBcsB1IBUD67Rz1Wprg+GOutO193jayO8DpRKooWC+r6bwtQxjt3nRUfwUl+X3a35QjxJlQpwis8kRy
Organization: New Artisans LLC

>>>>> Gabriel Scherer
>>>>> <gabriel.scherer AT gmail.com>
>>>>> writes:

> The fact that "map id = id" cannot be obtained by computation alone, so
> there seems to be little chance for Extraction to optimize it by itself.

Is there a way to emit literal text through the extraction mechanism, so that
I could emit GHC rewrite rules for transformation like this?

John

[Coq-Club] Question about Extraction, Ilmārs Cīrulis, 09/03/2015
- Re: [Coq-Club] Question about Extraction, Ilmārs Cīrulis, 09/04/2015
  - Re: [Coq-Club] Question about Extraction, Gabriel Scherer, 09/07/2015
    - Re: [Coq-Club] Question about Extraction, John Wiegley, 09/07/2015