coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Beta Ziliani <beta AT mpi-sws.org>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] How to FMapAVL.Make(N)?
Date: Fri, 5 Jan 2018 09:26:02 -0300
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=beta AT mpi-sws.org; spf=Pass smtp.mailfrom=beta AT mpi-sws.org; spf=None smtp.helo=postmaster AT jupiter.mpi-klsb.mpg.de
Ironport-phdr: 9a23:Gm+m5hBgEo85z7t7sVKgUyQJP3N1i/DPJgcQr6AfoPdwSPv/osbcNUDSrc9gkEXOFd2Cra4c0qyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUmTaxe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Qiqp4bt1RxD0iScHLz85/3/Risxsl6JQvRatqwViz4LIfI2ZMfxzdb7fc9wHX2pMRsZfWSJCDI2hcYUAE/EMMvxEo4TnvVYCsQeyCAuqCejyyjFInHj23agi3uk8Dw7GwBYvFM8Nv3TVqNX1Nb0dUea0zKLVyjjMdO1Z2Svn54XTdxAhufCMUatrccvf0kkjDQTFjk+fqYH8OT6ey+cDs3CD4uZ9W++ij3Qrpxx1rzS1xcohi5PFip8Vx1zc6yl13II4Kce7RUN7e9KoDoVcui+AO4drQM4vTWdlszsgxLIco560Zi0KxYwnxxHBb/yHdJCF4hD+VOaJIDd4mGxqeKilixa36Uigy/TwVsqw0FZRtSVJiNzMtmgC1xDJ98eIVONx/kan2TmRywDe8vxILE4wmKbBNpIsxqQ8m5kSvEjZAyP7mF36jKqMeUUl/uio5f7nYrLjppKELIB7lB3+Pb41l8y6GeQ4MxECX3OV+OSnzrHj+lf5QLpSgv0sjqbZqIzaJdgcpqOhHwBV1Z8j5w+jADeizdQXhmIKLElFeRKCl4jmIUvCIPH+DfelglSjii1nx/7cPu6pPpKYBX/a2JzlYLw1v0Vb0U84yc1Vz5NSELAIZvzpDBzfrtvdWzU0LwX88efjCdx718tKU2+TC4ecKKKXqkCToOU1LL/fN8cupD/hJq19tLbVhngjlApYJPHx0A==

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