coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Inductive Records, example needed.

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Inductive Records, example needed.
Date: Wed, 9 Sep 2015 21:11:05 +0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ilmars.cirulis AT gmail.com; spf=Pass smtp.mailfrom=ilmars.cirulis AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f178.google.com
Ironport-phdr: 9a23:PG5SQh1F/Z0Ovm//smDT+DRfVm0co7zxezQtwd8ZsegQLPad9pjvdHbS+e9qxAeQG96Lt7Qd16GP6v+ocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC04Lui6vrosKbSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBO/xeL19RrhFBhwnNXo07Yvlr1OLGQCI/z4XVngcuhtOGQnMqh/gCMTfqCz/48t53YKAJoXdTKopXTW5p/NqTBrhkjxBPD8j7WXWkeR/iatapFSqoBkpkN2cW52cKPcrJvCVRtgdX2cUBss=

Thank you much! :)

On Mon, Sep 7, 2015 at 2:55 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

2015-09-04 23:09 GMT+02:00 Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>:
Hello,

I tried to make Recursive Records, but I can't find any example. There's no hint in the Coq manual.

The best I could do was "

Inductive R := { head: nat; tail: R }.", but with without a Nil it has no use.
(For example, R -> False is trivial theorem. That means that no instance of this type could possibly exist. :( )

In inductive context, yes, but there is also the coinductive one.

Otherwise, you can also try:

Inductive R := { head: nat; tail: option R }.

Or trees:

Inductive R := { index:Type; chidren : index -> R }.
(leaves have index=emptySet)

Thanks in advance,
Ilmars

[Coq-Club] Inductive Records, example needed., Ilmārs Cīrulis, 09/04/2015
- Re: [Coq-Club] Inductive Records, example needed., Cedric Auger, 09/07/2015
  - Re: [Coq-Club] Inductive Records, example needed., Ilmārs Cīrulis, 09/09/2015