coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question about Extraction

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Question about Extraction
Date: Thu, 3 Sep 2015 14:52:10 +0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ilmars.cirulis AT gmail.com; spf=Pass smtp.mailfrom=ilmars.cirulis AT gmail.com; spf=None smtp.helo=postmaster AT mail-yk0-f178.google.com
Ironport-phdr: 9a23:MVmaGhwGHUWNlcHXCy+O+j09IxM/srCxBDY+r6Qd0ewSIJqq85mqBkHD//Il1AaPBtWHraoYwLaM+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStKU15j8i7r60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mooRLVry/dKAlR5RZCi4nOiY7/oej4RLEVE6E4mYWemQQiBtBRQbfukLURJD05wr+s0Fnw2GxPNfrSbEvEWCj66JiUgSugyYdKjo460nYj8VxiORQpxf39E83+JLdfIzAbKk2RajaZ95PHWc=

Is there a way to get simplified result of extraction?

For example, I have function that is extracted to "let F l = map (fun f -> f) l" that can be simplified to "let F l = l".

[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