coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to FMapAVL.Make(N)?

From: Beta Ziliani <bziliani AT famaf.unc.edu.ar>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How to FMapAVL.Make(N)?
Date: Fri, 5 Jan 2018 10:07:07 -0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bziliani AT famaf.unc.edu.ar; spf=None smtp.mailfrom=bziliani AT famaf.unc.edu.ar; spf=None smtp.helo=postmaster AT agni.famaf.unc.edu.ar
Ironport-phdr: 9a23:BPuaoB+4JrSdzP9uRHKM819IXTAuvvDOBiVQ1KB30ewcTK2v8tzYMVDF4r011RmVBdyds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+54Dfbx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsYSmpPXshfWS9PDJ6iYYQTFOcOJ/pUopPnqlcSsRezBw+hD/7vxD9SgX/22LU33vk/HgHaxgMrAtEBsHXQrNX0LqgSV+G1x7TPwDrYbvJW2DP96InSfRAnoPGBRrxwftDUyUY1GQPJlEiQqYr5MD+PyOsCrnWb4/B6WuK1kmMqrRx6rDaoxscpkIbJh4QVx0jF9SV/2oY1JMe3RFR1Yd6+FpZbqiKUN5NuT888X21kpDw2xqAHtJKhYSQHyo4rywPDZ/GHa4SE/A7vWeKLLTp7hH9pYqyziwu9/ES6yuDwS8+520tQoCVfiNnDrHUN2gTT6seZTvt9+V+s1iyA1wDV6+FIO040mrDeK5E7zL48jIcTsULfESPshkr5kbKWel8+9eiy8+jnY7PmqYGAN4JslA3yLrgiltaiDek5KAQCQmqW9f6h2LH//UD1WLBKgec3kqndvpDaP8MbpquhDgBO04cj6hK/Dza839QenHkKN1xFdwiCj4fzNVHCOu34DfGjjFi2jjhk2u3GMqf7DZXXNnTDiqvufa5h605Azwo+1cxQ55VNCr0YPP3zXlLxu8fDAx8iMw20xv7nB89n2oMfX2KPGK6ZP7nIvV+G/OJ8a9WLMaQSoX7WL+Uvr6rlimZ8klsAd4Go24EWYTa2BKI1DV+eZC/Gj8sIWVULugs3Su2i3FeQUDpSbnCzd6w14zg1Tp+gBsHOSp3riabXj3TzJYFfem0TUgPEKnzvbYjRHq5UMC8=

Great, thanks!

Is there any reason why N (or other structures) do not export themselves as OrderedTypes?

Best,

Beta

On Fri, Jan 5, 2018 at 9:49 AM, Frédéric Blanqui <frederic.blanqui AT inria.fr> wrote:

Hi Beta.

Perhaps you can solve your problem using https://coq.inria.fr/distrib/8.7.0/stdlib//Coq.Structures.OrderedTypeEx.html .

Best regards,

Frédéric.

Le 05/01/2018 à 13:26, Beta Ziliani a écrit :

Hi list,

Using the STD lib, I’d like to make a map with the N module as key. Despite N being a TotalOrder, Make complains that The field lt_not_eq is missing in Coq.NArith.BinNat.N. How should I proceed?

Many thanks,
Beta

[Coq-Club] How to FMapAVL.Make(N)?, Beta Ziliani, 01/05/2018
- Re: [Coq-Club] How to FMapAVL.Make(N)?, Frédéric Blanqui, 01/05/2018
  - Re: [Coq-Club] How to FMapAVL.Make(N)?, Beta Ziliani, 01/05/2018