coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] Faking induction-induction in Coq?
- Date: Sat, 11 Jul 2015 23:58:24 -0400
Hi,
Is there a (known) way to fake induction-induction in Coq?
Abhishek mentioned http://www.cs.ru.nl/~venanzio/publications/induction_recursion.ps last year as a way of faking induction-recursion in Coq. I'm curious, in particular, about how to define well-typed syntax for dependent type theory in Coq, and, more specifically, one that supports a quotation function, which sends any syntactic term to a syntactic representation of that syntax, i.e., sends (app 'S' '0'), the syntax representing the numeral 1, to (app (app 'app' "S") "0").
Thanks,
Jason
- [Coq-Club] Faking induction-induction in Coq?, Jason Gross, 07/12/2015
- Re: [Coq-Club] Faking induction-induction in Coq?, Thorsten Altenkirch, 07/13/2015
- <Possible follow-up(s)>
- Re: [Coq-Club] Faking induction-induction in Coq?, Thorsten Altenkirch, 07/13/2015
- Re: [Coq-Club] Faking induction-induction in Coq?, Bas Spitters, 07/13/2015
- Re: [Coq-Club] Faking induction-induction in Coq?, Gabriel Scherer, 07/14/2015
- Re: [Coq-Club] Faking induction-induction in Coq?, Ralph Matthes, 07/24/2015
- Re: [Coq-Club] Faking induction-induction in Coq?, Thorsten Altenkirch, 07/14/2015
- RE: [Coq-Club] Faking induction-induction in Coq?, Soegtrop, Michael, 07/15/2015
- Re: [Coq-Club] Faking induction-induction in Coq?, Bas Spitters, 07/15/2015
- RE: [Coq-Club] Faking induction-induction in Coq?, Soegtrop, Michael, 07/15/2015
- Re: [Coq-Club] Faking induction-induction in Coq?, Fredrik Nordvall Forsberg, 07/14/2015
- Re: [Coq-Club] Faking induction-induction in Coq?, Eddy Westbrook, 07/14/2015
- Re: [Coq-Club] Faking induction-induction in Coq?, Gabriel Scherer, 07/14/2015
- Re: [Coq-Club] Faking induction-induction in Coq?, Bas Spitters, 07/13/2015
Archive powered by MHonArc 2.6.18.