coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Tej Chajed <tchajed AT mit.edu>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Extraction of int31 to ocaml int
- Date: Mon, 12 Feb 2018 13:50:30 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tchajed AT mit.edu; spf=Pass smtp.mailfrom=tchajed AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-2.mit.edu
- Ironport-phdr: 9a23:XZ+5GhLPZ4fTuFa179mcpTZWNBhigK39O0sv0rFitYgRKfXxwZ3uMQTl6Ol3ixeRBMOHs6sC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffxhEiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhyUJNzA5/m/ZidF+grxHrx+6vRNz35TZbZuJOPZifK7Qe84RS2pbXsZWUixMGp2yYJUND+EcI+tYr5Pyp1kQohSjGAKhA//vxSNIhnDs3601zfkuHBrD3AwhA9ICqmrbo8joNKoLV+2+0afGzTLGb/xM2Df97pDFch8gofGQXbJwbNHexVMzGAPCi1Wdr5HuMTCN1ukVrmSW7PBsWOa1h2I5qwx9uCWjy8k0hoXXmo4YzkrI+CZ5zYovO9G0VUx2bcS5HJZStCyXMZZ9TNk4TGFyoik6z6ULuZ6lcygOz5Qq3wPQa/mGcoSR5xLsTueRITNjhH17ZL2zng2y/lS6xe36UMm7zkxKojNbntXWs3AN1gDT5tKZRfRg40etwTeP1wbN5eFYOU04iKnWJ4Qlz7IqiJYesV7PEjL4lUnuia+ZbEQk+uym6+T9ZbXmo4eRN5NohQH+KKsumNKwDvkjPwgLXmib5f6w26P+8k3kWLlKlOE5krHFsJDGIsQWvrK2AwhM0oo69xm/Cyqm388DkHkcLFNFfQqHgJLzN1HPJvD4F/a/jE62nDdl3fCVdoHmV57KNz3IlKrrNeJ27FcZww4ux/he4YhVA/cPOqSgdFX2sYnkAx1xGAy9wevrQIFh3YMXW2+DKqqYLOXfvULetbFnGPWFeIJA4GW1EPMi/fO71SZoy29YRrGg2N4sUF79G/1nJ0uDZn+90NIADSEHshdsFbW22m3HaiZaYjOJZ4x5/isyWdCjDJuFS4yw0uTYgXWLW6ZOb2UDMWiiVHflc4LfAqUAbTDXJ8ZglicJXv26QIYn0xy08VW8zrt7aOfY539AuA==
I don’t see Int31 specifically in the standard library so it does seem like you have to write it, but you can base your implementation off of ExtrOcamlNatInt.v and ExtrOcamlNatBigInt.v in theories/plugins/.
On Mon, Feb 12, 2018 at 1:41 PM, Helmut Brandl <helmut.brandl AT gmx.net> wrote:
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)?RegardsHelmut
- [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.