coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Trivial? proof on a simple inductive type

From: Brandon Moore <brandon_m_moore AT yahoo.com>
To: franck.barbier AT franckbarbier.com, coq-club AT inria.fr
Subject: Re: [Coq-Club] Trivial? proof on a simple inductive type
Date: Tue, 8 Mar 2011 10:18:07 -0800 (PST)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=Message-ID:X-YMail-OSG:Received:X-Mailer:References:Date:From:Subject:To:In-Reply-To:MIME-Version:Content-Type; b=eJc4pnqai6rGj6RAASzub7BeBHBSvxVR6IG6Tsfr6yqJZpMUAOdvMnR4iNgDyoGTpkqtl91Jn8sPh5OeE/h6TPI1YHqEN7Ww9DZoba8sIfpVifREN8bLYVVSRngQnbS95kkvHIbD2aB2n7mnYjl2Mm17mikmTjuZnPE9l1pWaoY=;

This seems to be related to the problem of proving that
terms in an injective type are acyclic. There is a nice
construction in McBride, Gougen, and McKinna's paper
"A Few Constructions on Constructors".

[Coq-Club] Trivial? proof on a simple inductive type, franck . barbier
- Re: [Coq-Club] Trivial? proof on a simple inductive type, Sylvain Heraud
  - Re: [Coq-Club] Trivial? proof on a simple inductive type, Sylvain Heraud
- Re: [Coq-Club] Trivial? proof on a simple inductive type, Brandon Moore
- Re: [Coq-Club] Trivial? proof on a simple inductive type, Adam Chlipala
  - Re: [Coq-Club] Trivial? proof on a simple inductive type, Vincent