coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Kenneth Roe <kendroe AT hotmail.com>
- To: Coq-Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Looking up definitions from inside an ml plugin
- Date: Thu, 16 Nov 2017 15:34:11 +0000
- Accept-language: en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=Pass smtp.mailfrom=kendroe AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM03-CO1-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:T8zsYxHdEvU2MhvUxTEplp1GYnF86YWxBRYc798ds5kLTJ76ocmwAkXT6L1XgUPTWs2DsrQf1LqQ7viocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TXhpQIVTz74LE9eIvn/UtrZiN3y3OSv8bXSZR9JjXyze+UhAg+xqFDyu88QjJdiYpw2x1OdoXZOd/5RyEtoIk6Wlhf4oMy3+cgwoGxrp/s9+psYAu3BdKMiQOkAAQ==
- Spamdiagnosticmetadata: NSPM
- Spamdiagnosticoutput: 1:99
I am developing an ml tactic, "arewrite". Inside a Coq source file where I use the tactic, I have the following code:
Require Import AdvancedRewrite.advancedRewrite.
Inductive x := | Const : nat -> x | XX : x -> x -> x.
Theorem test7: forall x, x=Const 4.
Proof.
intros.
arewrite.
Abort.
From inside the "arewrite" ml source code, I have the following code to try and lookup the definition of "x":
let i = ... s ... (* s contains the string "C_Top.x" *)
let d = Environ.lookup_mind i env
Can someone fill in what I need for the first line to properly form the identifier "i"?
- Ken
- [Coq-Club] Looking up definitions from inside an ml plugin, Kenneth Roe, 11/16/2017
- Re: [Coq-Club] Looking up definitions from inside an ml plugin, Talia Ringer, 11/16/2017
- Re: [Coq-Club] Looking up definitions from inside an ml plugin, Talia Ringer, 11/16/2017
- Message not available
- Re: [Coq-Club] Looking up definitions from inside an ml plugin, Kenneth Roe, 11/17/2017
- Re: [Coq-Club] Looking up definitions from inside an ml plugin, Talia Ringer, 11/17/2017
- Re: [Coq-Club] Looking up definitions from inside an ml plugin, Kenneth Roe, 11/19/2017
- Re: [Coq-Club] Looking up definitions from inside an ml plugin, Matthieu Sozeau, 11/19/2017
- Re: [Coq-Club] Looking up definitions from inside an ml plugin, Kenneth Roe, 11/19/2017
- Re: [Coq-Club] Looking up definitions from inside an ml plugin, Talia Ringer, 11/17/2017
- Re: [Coq-Club] Looking up definitions from inside an ml plugin, Kenneth Roe, 11/17/2017
- Message not available
- Re: [Coq-Club] Looking up definitions from inside an ml plugin, Talia Ringer, 11/16/2017
- Re: [Coq-Club] Looking up definitions from inside an ml plugin, Talia Ringer, 11/16/2017
Archive powered by MHonArc 2.6.18.