coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Constructing a match expression inside an ml tactic

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Constructing a match expression inside an ml tactic
Date: Fri, 13 Oct 2017 14:07:21 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
Ironport-phdr: 9a23:fRlrlRYhAXigSlgNz5oRPob/LSx+4OfEezUN459isYplN5qZpsm9bnLW6fgltlLVR4KTs6sC0LWG9f24EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i76vnYuHUD0MhMwLeDoEKbTid623qa84c79eQJN0Re7e7J5K12KpB7Kt4FCjI14K602jAfAuWBJU+VQ32JhY1yJyUWvrvys9YJupnwD88kq8NRNBP33

On Mon, Oct 09, 2017 at 01:42:54AM +0000, Kenneth Roe wrote:
> let ci = make_case_info Global.env ind RegularStyle in
>
> mkCase (ci, tterm, eterm, Array.of_list terms)
>
> The "ci" field seems to contain information I need to pull from the
> global environment. I was able to figure out the first and third
> parameters by looking at pieces of code in Coq. However, I'm not able
> to figure out what to do with the "ind" field. What do I fill in for
> ind?

It is an inductive type. This is how I do:

https://github.com/LPCIC/coq-elpi/blob/master/src/coq_elpi_HOAS.ml#L644

In that code I know rt is a spine of lambdas ending with an applied
inductive type. This is also relevant

https://github.com/coq/coq/blob/master/kernel/names.mli#L390

My 2 cents,
--
Enrico Tassi

[Coq-Club] Constructing a match expression inside an ml tactic, Kenneth Roe, 10/09/2017
- Re: [Coq-Club] Constructing a match expression inside an ml tactic, Enrico Tassi, 10/13/2017