coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
Archive powered by MHonArc 2.6.18.