The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

On Fri, 16 Apr 2004, Robert T Bauer wrote:

> Hi,
> 
> I have the following deep embedding in hol and want to convert it to coq:
> 
> Hol_dataype `e = L of num | V of string | E of e => e`
> 
> I can live without strings - so that Hol_datatype `e = L of num | V of num 
> | E of e => e`
> works quite well for me.
> 
> I think this needs to be defined as mutually inductive type in coq.
> 

Unfortunately there is no string in Coq at the moment. I've been using a
library for String in Coq 7.4 that was directly inspired by the one of HOL
but I'ven't succeeded yet in converting it to Coq 8.0. The version for Coq
7.4 of the library is available at:

ftp://ftp-sop.inria.fr/lemme/Laurent.Thery/String.tar.gz

Using natural numbers instead, your definition in Coq is direct: 

Inductive e: Set :=
  L: nat -> e
| V: nat -> e
| E: e -> e -> e.

--
Laurent Thery