coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq term trees

From: Jónathan Heras <joheras AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Coq term trees
Date: Wed, 8 Jan 2014 14:55:33 +0000

Hi,

When working in first-order logic, we can represent terms as term-trees as given in e.g. Terese.
I am currently working with Coq terms, and I wonder if there is a "standard" definition for term-trees of Coq terms.

Best,
Jonathan

[Coq-Club] Coq term trees, Jónathan Heras, 01/08/2014