coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: <saulo2 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Beginner Question
- Date: Sat, 08 Nov 2014 16:53:18 +0100
Hi,
I am trying to port a defitional interpreter for a small DSL from Standard ML
to Coq. The first problem I am facing is how to define self referential values
in Coq. Thats what I am trying to do:
Require Import String.
Open Scope string_scope.
Inductive OBJECT : Type := Object : CLASS -> list (string * OBJECT) -> OBJECT
with CLASS : Type := Class : list (string * CLASS) -> CLASS.
Definition MediaType := Class nil.
Print MediaType.
Definition File := Class (cons ("mediaType", MediaType) nil).
Print File.
Definition User := Class (cons ("picture", File) nil).
Print User.
Definition Message := Class (cons ("sender", User) (
cons ("recipients", User) (
cons ("replies", Message) nil
)
)
).
Print Message.
but the Coq complier complains "Error: The reference Message was not found in
the current environment."
I had the same problem with the Standard ML version of the interpreter. In
this version, I was able to overcome the problem with references (refs).
Does anyone know how to solve the same problem in Coq?
Thanks in advance,
Saulo Medeiros de Araujo
- [Coq-Club] Beginner Question, saulo2, 11/08/2014
- Re: [Coq-Club] Beginner Question, Jonathan, 11/08/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/08/2014
- Re: [Coq-Club] Beginner Question, Jonathan, 11/08/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/08/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/09/2014
- Re: [Coq-Club] Beginner Question, Jonathan, 11/09/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/09/2014
- Re: [Coq-Club] Beginner Question, Jonathan, 11/09/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/09/2014
- Re: [Coq-Club] Beginner Question, Pierre Casteran, 11/09/2014
- Re: [Coq-Club] Beginner Question, Jonathan, 11/09/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/09/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/08/2014
- Re: [Coq-Club] Beginner Question, Jonathan, 11/08/2014
- Re: [Coq-Club] Beginner Question, Saulo Araujo, 11/08/2014
- Re: [Coq-Club] Beginner Question, Jonathan, 11/08/2014
Archive powered by MHonArc 2.6.18.