Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Faking induction-induction in Coq?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Faking induction-induction in Coq?


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page