coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] need help converting hol proof to coq.

From: Robert T Bauer <rtbauer AT us.ibm.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] need help converting hol proof to coq.
Date: Fri, 16 Apr 2004 11:57:41 -0700
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.

thanks

[Coq-Club] beta-expansion tactic?, Josh Berdine
- [Coq-Club] need help converting hol proof to coq., Robert T Bauer
  - Re: [Coq-Club] need help converting hol proof to coq., Thery Laurent