coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Inductive Records, example needed.
Date: Sat, 5 Sep 2015 00:09:04 +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-yk0-f176.google.com
Ironport-phdr: 9a23:X/72rRaV8dOxvUjJVyV5AAv/LSx+4OfEezUN459isYplN5qZpcq8bnLW6fgltlLVR4KTs6sC0LqK9fi+EjVdvt6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDuvcWNKFwV23KUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtB7dfFXEtN30/zMztrxjKCwWVrDNIWWIP1xFMHgLt7RfgX563vDGs5cRn3yzPHMnz5qovER+j9bpvSQSg3CYDMjcj6yfci9ZtiKNAiB2krh17hYXTZdfGZ7JFYqrBcIZCFiJ6VcFLWnkZDw==

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. :( )

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