coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

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

[Coq-Club] ml plugin: obtaining the type of an expression, Kenneth Roe, 04/21/2018
- Re: [Coq-Club] ml plugin: obtaining the type of an expression, Gaëtan Gilbert, 04/21/2018