Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] ml plugin: obtaining the type of an expression

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] ml plugin: obtaining the type of an expression


Chronological Thread 
  • From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] ml plugin: obtaining the type of an expression
  • Date: Sat, 21 Apr 2018 11:39:57 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay10.mail.gandi.net
  • Ironport-phdr: 9a23:s2Ybvhex3GxZKCdfvH0gOoPilGMj4u6mDksu8pMizoh2WeGdxcuyZB7h7PlgxGXEQZ/co6odzbaO6Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahb75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM37X/ZisJwgqxYrhyuqRNwzIzIb4+aL/d+YqDQcMkGSWZdUMtcVypMCZ68YYsVCOoBOP5VoYjnqFwSsRuxHw+sC/vuxD9Jgn/5xrM10/49EQrb2wEgEMgBv2rIrNrvMqceS++1zKjMzTrYcfxWwyv95ZPTchAiofCMRrFwccvUyUkqCQzFlE+cqYr7MDOJz+kAtXWQ4el4Ve+3lWIrtgN8riKty8swkIXFm4AYx1Pe+Slnzos5OcW0RU9lbdK+DZdcqz+WO5FrTs4tQGxkojs2x78GtJO9YSME0o4oxwTFZPyCa4WI4gzsVOKWITpgnnJqZra/iAyy8ES91uHwTMy030xLripBiNXMuWoC1xrO5ciGUPd9+Fmu2SqX2wDS7OFLP1w0mLLFJ5I8wLM8jJgevVjZEiPrmkj7j7Waelsq9+S08+jnZ6/ppp6YN496kAH+NaEul9SwAesiLAcOQ3KU+eKm2L3s/E35RK5FgeMskqnFq53aPscbp66iAw9W04Yj7hO/ACm80NgCm3kIMk5FdAqdj4f1I1HOPOz4DfCnjluwlzdr3unKMaHlApXQNXfOi6zhfLZ4605E0gU/19Ff55ROCrEAOv3/QEHxtMaLRiM+Zgez2qPsDMh3/oIYQ2OGRKGDY43ItlrdyeusP+CKU6AUvDzwMeRts/HngGMwnxkSfK2j0IELQGu7D+9lIkCcbGCqhNodRzRZ9jEiRfDn3QXRGQVYYGy/Cvplt2MLTbm+BIKGfbiDxbmI3SO1BJpTPz4UEVOdCnTpcoCJQbEKZT7Ae5Y9wAxBbqCoTsoa7T/rrBXzkuQ1NenF4S4ZsJfuzp5z6vGBzUhvpwwxNNyU1iS2d08xnm4MQGVqjrpypUVskw/F1KF5h7pXHNpf5rVPXxtobZM=

Look at the Retyping module (if you already know your term is well typed) and the Typing module (if you want to check that it's well typed, including generating universe constraints)
(both are in the pretyping/ directory)

Gaëtan Gilbert

On 21/04/2018 06:10, Kenneth Roe wrote:
Is there an OCaml function in the Coq source tree I can call to obtain the type of an expression?  I'd like to be able to do something like:


let (type_of_expr:types) = <type_call>(env:Environ.env) (trm:types)


                 - Ken




Archive powered by MHonArc 2.6.18.

Top of Page