coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to use ExtrOcamlZBigInt?

From: Yishuai Li <yishuai AT cis.upenn.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] How to use ExtrOcamlZBigInt?
Date: Tue, 14 Aug 2018 16:32:51 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=yishuai AT cis.upenn.edu; spf=Pass smtp.mailfrom=yishuai AT seas.upenn.edu; spf=None smtp.helo=postmaster AT mail-io0-f171.google.com
Ironport-phdr: 9a23:J5aIwxyb0XNlUwTXCy+O+j09IxM/srCxBDY+r6Qd1O8eIJqq85mqBkHD//Il1AaPAd2Fraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HSbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHohikJNCM3/n/LhcFrlq1XvAisqgZjz4LIYoyYMud1cKPHfdMdQGpMRsReVy1aAoO8cosAFesBNvteoYn8ulADqhu/BQi3BOPv1z9HnH720LYm3OQgCgHKxhEgH8oQv3TSqtX5LrkdXv2ozKTRyzjIcv1Y2TD46IfScxAhp+mBXbN2ccrLyEkgDRnJjluKqYHjIjib1fwNvnCF4+Z8Ue+jkW0qpgFrrjSx2MshhJPFip8Xx1zZ7Sl13po5KNmiREN4YdOoCoVcuz+UOodsX88vQW9ltSAnwbMco5G7ZjIFyJE/yh7fdfOHd4+I7wrmVOmLIDd4gGtpeLO4hxqu6ESgxPDwW8up3FpQoSpFld7Mtn8J1xPN8MSIVvx9/kK51TaO0QDc9P1ELFgqmabHL5Mt2L09m5oJvUjdACP7ll/6gLKUe0k54uSo7v7oYrTipp+SLY90jQT+P7wum8y+GuQ4MhUOUHKa+emnz73s41f2QK5Qgv0riqnWrpbaJcIBqqGnHgBVz54v6wyjADe+zNQYgX4HIUpZdxKAlojlIk3BIPTlDfikmFmsizdqx/XePrL7GJnNL37DkK3gfbln8UJcxhAznphj4MdfDahEK/buUGfwssbZB1k3KV+a2eHiXeR8zYMDUGPHJq7RZLLTql+V7+MHKOiXIpINtTD7bfUp+qi93jcChVYBcPzxjtMsY3eiE6E+ehTLUT/Xmt4EVFwykE87Re3uhkeFVGcNNW2/Vrl6+yk2DoTgAIveFNn03O6xmRyjF5gTXVhoT0iWGC61JY6FQLERcC+UJIlsniFWDeH8Gb9k7gmnsUrB85QiLufQ/XdG55fq1dww5uqL0B9rqmUyAMOa3GWACWpzmzFQSg==

Dear Coq Club,

ExtrOcamlZBigInt extracts Z to Big.big_int, but where is the Big module?

Thanks,

Yishuai

[Coq-Club] How to use ExtrOcamlZBigInt?, Yishuai Li, 08/14/2018