coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Derivation tree of a term (or "pseudo-term" ?)

From: Jérémy Hervé <jeremy.herve AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Derivation tree of a term (or "pseudo-term" ?)
Date: Tue, 9 Aug 2016 18:42:36 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jeremy.herve AT gmail.com; spf=Pass smtp.mailfrom=jeremy.herve AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f45.google.com
Ironport-phdr: 9a23:DWG96B1sMXpR4rqBsmDT+DRfVm0co7zxezQtwd8ZsegTLPad9pjvdHbS+e9qxAeQG96KsrQc0qGO4uigATVGusfZ9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oMyKJV0Rz2LsKfMqdVPt/F2X7pFXyaJZaY8JgiPTpXVJf+kEjUhJHnm02yjG28Gr4ZR4+D5Rsf9yv+RJUKH9YrhqBecAVGduYCgJ45jgsgCGRg+S7FMdVH8Xm1xGGVvr9hb/C7VwqKr/p6Jd1TOEvIWiT70uVDGzqadmUgHloCgCPj89tmrQj5oj3+pgvBu9qkknkMbva4aPOa8mcw==

Hello everyone,

I am googling on this subject since near an hour, browsing the Coq manual failing to find any information on the subject.

I have to precise I am still a begginer, and without any academic background.

I understand that Coq has his type system in the lambda-C corner of the Barendregt lambda-cube, where Sorts are Set, Prop and Type_i, Axioms are (Set: Type), (Prop:Type), (Type_i:Type_i+1), where Rules are (Prop, Prop, Prop) ... etc.

It's quite easy, using pen and paper, to draw for example the derivation tree that build the identity function.

Since I am very interested in understanding the fundation of Coq, I would be happy to find a command showing this derivation tree in some format...

Thanks in advance,

Best regards,

Jérémy Hervé,

Nantes, France

[Coq-Club] Derivation tree of a term (or "pseudo-term" ?), Jérémy Hervé, 08/09/2016