coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Int63, simplification and native computation

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Int63, simplification and native computation
Date: Sat, 6 Apr 2019 12:15:38 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga18.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.400.15
Ironport-phdr: 9a23:6mMlsxbIU8b56yop5GP7+7z/LSx+4OfEezUN459isYplN5qZr8W9bnLW6fgltlLVR4KTs6sC17OP9fixEjBeqdbZ6TZeKcQKD0dEwewt3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9FYHdldm42P6v8JPPfQpImCC9YbRvJxmqsAndrMYbjZZ/Jqor1hfEpnREdutXyGh1IV6fgwvw6t2/8ZJ+7yhcoe4t+9JFXa7nY6k2ULtUASg8PWso/sPrrx7DTQWO5nsYTGoblwdDDhbG4h/nQJr/qzP2ueVh1iaUO832Vq00Vi+576h3Uh/oiTwIOCA//WrKl8F/lqNboBampxxi347ZZZyeOfRicq/Be94RWGxMVdtTWSNcGIOxd4sBAfQcM+ZEoYfzpFUOohm/BQawC+zi0SVHimPy0KAgz+gtDR/K0Qo9FNwOqnTUq9D1Ob8cXe6oy6nH0zrDb+9M2Tf68IjEag0qr/aNXb1sccre01cgFwfLgl6NroHlOjKV2fgNs2eB8eVgUfiji3Ugqw5vrTiv2t0sio7Rho8Oy1DE8zl5z5gxJdGiVEF7ZtukHYJWuiqHOYV2RcYiTHtpuCY80rAGuJi7fDQUx5Qj3RLQduKIfo6V6RzgTOacOSp0iXxqdb6lmhq//0etxvfhWsS60VtGtDdJnsfNu3wVyhDe68aKRuFz80qvwzqDyQ7e5+VeLUwplqfXNoYtzqMxm5cXq0jPAC/7lUrsgKOIbEko5PWk5uL6abv8vJCcLZV7igTmP6QuhMO/BeM4PxALX2iU4+uwyb7u8Vf4QLVMkv05jK3ZvIrGKsQco661Gw5V0oA95BajFzqqzdoVkHYdIF5Ydh+KgJLlN0zALf35F/uznkqgnTZzy/DDJLLhA5HNLnbZkLfmeLZw80tcyAsvwtBf/Z1bFLUBLOjoWk/2qtPYAQM5Mxazw+b/E9h914UeWX6RDa+dKq/drViI5uc3L+mWeIAVoCr9K+Qi5/P2kXA5nkYdcbC10psTdXC3Be9rI16ZYHrpmtcOC30Gvgs4TOzwiV2NSyRfZ3ioX/F02jZuQomhFMLIQp2nqL2HxiayWJNMLCgSAVeVVHzsao+sWvEWaSvULNU3wRIeUr30AbQm2B6yrgjij/JCL+HU8yAc/9q30dl+5+TekVcp8jF7E96ay0mMSX15miUDQDpgj/M3mlB01lrWifswuPdfD9EGv6oYADd/DobVyqlBM/63XwvAetmTT1P/G4enBy08SpQ6xNpcOh8hSeXntQjK2m+RO5FQj6aCXcVm86TA0ny3LMF4mS6fifsRymI+S84KDlWIw65y8w+KWNzMnEzAx+Crc7gR2GjG82LRlWc=

Dear Coq Club,

I just wanted to note that cbn instead of simpl works fine (as usual) – I somehow mixed up cbv and cbn in testing.

So:

Require Import Int63.

Require Import ZArith.

Goal Int63.to_Z 1 = 1%Z.

cbn.

Does the simplification as expected.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Int63, simplification and native computation, Soegtrop, Michael, 04/05/2019
- RE: [Coq-Club] Int63, simplification and native computation, Soegtrop, Michael, 04/06/2019