coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A plugin to disable positivity check, guard check and termination check

From: Simon Boulier <simon.boulier AT inria.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] A plugin to disable positivity check, guard check and termination check
Date: Thu, 21 Jun 2018 09:40:51 +0100
Openpgp: preference=signencrypt

Dear all,

I made a plugin to experiment with type in type, non positive inductive
types and non terminating fixpoints:

https://github.com/SimonBoulier/TypingFlags

Enjoy!

Simon Boulier

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] A plugin to disable positivity check, guard check and termination check, Simon Boulier, 06/21/2018
- Re: [Coq-Club] A plugin to disable positivity check, guard check and termination check, Talia Ringer, 06/22/2018