The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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