coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Is there a nominal package for Coq?

From: Enrico Tassi <Enrico.Tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Is there a nominal package for Coq?
Date: Fri, 06 Dec 2019 12:54:55 +0100

Dear Coq-Club,
I was looking for some "nominal package" for Coq.

I could find Metalib (https://github.com/plclub/metalib) but, as far as
I could understand, it does not synthesize axioms for alpha conversion
(said otherwise it does not provide a syntax to write ADT with binders,
hence it can't synthesize for you much). If I'm wrong please correct
me.

Otherwise, is there another package giving some support for nominals?

Best regards,
--
Enrico Tassi

[Coq-Club] Is there a nominal package for Coq?, Enrico Tassi, 12/06/2019
- Re: [Coq-Club] Is there a nominal package for Coq?, Danil Annenkov, 12/06/2019
  - Re: [Coq-Club] Is there a nominal package for Coq?, Frédéric Blanqui, 12/06/2019
  - Re: [Coq-Club] Is there a nominal package for Coq?, Tadeusz Litak, 12/10/2019