coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Kenneth Roe <kendroe AT hotmail.com>
To: Coq-Club <coq-club AT inria.fr>
Subject: [Coq-Club] ml plugin: obtaining the type of an expression
Date: Sat, 21 Apr 2018 04:10:32 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=Pass smtp.mailfrom=kendroe AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM03-BY2-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:pOkc0xa/kNmo4nZTht1YFOP/LSx+4OfEezUN459isYplN5qZoMuybnLW6fgltlLVR4KTs6sC17KN9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCazbL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjA57m/Zl9BwgqxYrh29qBNy2JTbbJ2JOPdkYq/RYc4WSGxcVchRTSxBBYa8YpMKAeUfO+ZYqZfyp0cOrRCjGQesA/3gwSJPi3/1w6I61fkuERvB3AM+BN8OsHPUrMnwNKgIUOC1yLPEwinEb/NTwDrw7pXDfBM5ofyUUr98bdDdxE0xGw/fj1ics4joMjeN2uQDrWeW7PZsWOeqhmMpqAx9vDyiy8I2hYbTho8YzlXJ+jlkz4kpO9K1TUF2bsOlHZRLsSyRKpF4Tdk4Q25yvSY30r0GtoC/fCgN0Jkp3wLSZfubf4WG+x7uSeSeLSlhiHJiY72wmQy+8U+9yu3gTca010tKrixYndXWrnANzRvT6tSZRfRh4keh2DGP1wbJ5uFDPEA0ia7bK5kmwr4zjJYcrUPDHirulEX3iq+ZaFkk9/Cn5uj7eLnrooGQO5V1hw3kNqkjntSzAeEiPQgPW2ib9/681Lrm/UDhQ7VFkPs2nbTDsJDdO8sWva65AwhJ0oYm8Rm/DjOm3M4EknkAKVJJYAiHgJTxO1HSPPD4Cu+yjEirkDdy3vzJIrnhAojWIXXYi7fgfbN961ZGxwYpzNBf4YhUCrAbL/7pVE/xro+QMhhsGAuths3jFd81gogZQCeEBrKTGKLUq16BoOw1dbqifogQ7RXwLf4o+/6mt3g00QsecK+lx5waQHC/AvFvIkHfan3p1IRSWVwWtxYzGbS5wGaJViReMi7rDvAMowojAYfjNr/tA4WkgbiPxiC+R8YEZmdaD1mNFTHjcIDWAq5QOhLXGddol3k/bZbkU5UojEr8tAjmzrNmKqzf/ShK7cu+hugw3PXakFQJzRIxD8mZ1D3SHUdduztTAhUHhuV4q0E7zUqf269lhfAeDcZU+/5CTgY9M9jb0vB+DNfxHAnGe4XQRQ==

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