coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Frédéric Blanqui <frederic.blanqui AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How to FMapAVL.Make(N)?
Date: Fri, 5 Jan 2018 13:49:58 +0100

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