Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Beginner Question

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Beginner Question


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page