coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] looking for test cases fore dependent decide equality

From: Jonathan Leivent <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] looking for test cases fore dependent decide equality
Date: Wed, 27 Jul 2016 12:03:36 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f169.google.com
Ironport-phdr: 9a23:bH48RBNEu4uM8nTOkN0l6mtUPXoX/o7sNwtQ0KIMzox0KPvyrarrMEGX3/hxlliBBdydsKMczbSL+PG4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuS9aU0Zn8hrj60qaQSj0AvCC6b7J2IUf+hiTqne5Sv7FfLL0swADCuHpCdrce72ppIVWOg0S0vZ/or9ZLuh5dsPM59sNGTb6yP+FhFeQZXwIPaD9uoZW3/VmeFUrcrkcbB04Ri1JjBxXPpEXxWY60uS/nvMJ83jObNIv4V+Zndy6l6vJJTxnhlCcOMXYd/WDJh8psxPZZpxSgpBF7zoP8b4ScNf44daTYK4BJDVFdV9pcAnQSSri3aJECWq9cZes=

I have made some progress on a dependent version of decide equality - one that can work with or without axioms:

https://github.com/jonleivent/deptacs

But it very much needs better tests. Would anyone like to donate some complex dependent inductive types they have as test cases?

Thanks very much in advance!

-- Jonathan

[Coq-Club] looking for test cases fore dependent decide equality, Jonathan Leivent, 07/27/2016