coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Helmut Brandl <helmut.brandl AT gmx.net>
- To: Coq-Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Extraction of int31 to ocaml int
- Date: Mon, 12 Feb 2018 12:41:30 -0600
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=helmut.brandl AT gmx.net; spf=Pass smtp.mailfrom=helmut.brandl AT gmx.net; spf=None smtp.helo=postmaster AT mout.gmx.net
- Ironport-phdr: 9a23:1cWScxXfyW7KFRwcOl2cvrMZ+PXV8LGtZVwlr6E/grcLSJyIuqrYYxCDt8tkgFKBZ4jH8fUM07OQ7/i5HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9vIBmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XhMJ+j79Vrgy9qBFk2YHYfJuYOeBicq/Bf94XQ3dKUMZLVyxGB4Oxd4kBAPQFPeZdson9u0YFoAakBQa2AuPg1ztIjWLx0K06zeshFQTG3BE8H94Uq3vUts/6NKEPXuCx16TIwjDDbvxM1Tf79ofIbgksrPeRVrxzacrc0VcjGx7bglmKt4DpITGY2v4Qv2WZ9eZsS/6jh3Y5pw1tpjWj3MQhh4nTio4I1FzJ9j91zJs3KNGlTkNwfMSqH4FKty6AMot7WsMiTH9suCY90rAGvJm7fDUWyJg9yB7fbvOGf5KO4h39SOadOTZ4hHR7d7Kjnxu+71WsxvPmWsWqzlpHrDBJnsTOu3wXyRDf9tCLSv5n8Ueg3TaP2RrT6uZBIU0slarUNZohwrstlpoPq0jMBTX2l1/wjKCLckUp4eeo6+HoY7n8oJ+TKZN0hhnkMqsygsy/Hfg4Mg8WUmeH/uS8zaTv8lH9QLVXlfI7ibLZsZDfJcQDvKG1GQ5V0oA56xa+FTiqytoYnWNUZG5CLTmAls3CP0zEaKTzCu76iFCxmh9qwerHN/vvGMOeFHXblKbdeuN95kpZ1RZ1x8pW4Z5QIr4EMLT1V1OimsbfC0oZPgix3vqvIs900I8aETaPD6ucLb+Uu0WB4O4rC+aJdMkTtSqreKtt3OLnkXJswQxVRqKux5ZCMCnpTMQjGF2QZD/XuvlEFG4LugQkS+m72lKHQXhVamrgBvtgtAF+M5qvCML4fq7omKaIjXW0G40QYG1aWAjVTCXYMr6cUvJJUxq8Z89sljtdCeqkTJI9kx6rpEn8xqY1duc=
Hello coq-clubbers.
I have found in the coq library the type int31 which seems to describe the semantics of ocaml int properly.
Is it possible to extract int31 to int in a way that the extracted program uses the fast computations of ocaml int? Probably the answer is yes. But is the proper set of extraction commands already available or do I have to create them on my own (with all the possibilities of making errors which coq cannot detect)?
Regards
Helmut
- [Coq-Club] Extraction of int31 to ocaml int, Helmut Brandl, 02/12/2018
- Re: [Coq-Club] Extraction of int31 to ocaml int, Tej Chajed, 02/12/2018
Archive powered by MHonArc 2.6.18.