coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Type checking in the presence of fixpoints on type indices

From: Ben Horsfall <ben.horsfall AT gmail.com>
To: coq-club AT inria.fr
Cc: Harald Søndergaard <harald AT csse.unimelb.edu.au>
Subject: [Coq-Club] Type checking in the presence of fixpoints on type indices
Date: Tue, 26 Oct 2010 17:13:57 +1100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:cc:content-type; b=UQuAEH66RUJAn/FI9Lv6b81NUUV1GO2XUEFiAdWzCPSDGUt+cteunWnwt635BUhkpj m9I61Mkifa/eDGGJUWIcwY1U2AeiqBjP4gqm0OrQA1iJQ49H0g8gUeZlS5xSxgxDK35a ykhIIayc0AilptAS0PNyzbHTbptQSP17LP7N0=

Suppose I'm trying to define an inductive relation on terms that have
an indexed type (i.e. Inductive tm : ty -> Set), and I have also
defined some Fixpoints f, g (let's say of type ty -> ty for
simplicity). Suppose also that I know that f x == g y (decidable
equality). Is there a way to induce the type checker to unify types tm
(f x) and tm (g y)? This should not require the fixpoints to be
computed during type-checking, only judicious use of a known equality.
Or is there a better way to approach this kind of difficulty?

Ben

[Coq-Club] Type checking in the presence of fixpoints on type indices, Ben Horsfall
- Re: [Coq-Club] Type checking in the presence of fixpoints on type indices, Adam Chlipala