The Coq mailing list

[Filou Vincent <vincent.filou AT gmail.com>]

You're missing the fact that the FMapAVL.Make functor expects a module 
compatible with the OrderedType module type,
and this type requires the definition of the "lt" field, representing 
the order relation.

I don't know nothing about extraction, but if you absolutely want to use 
Ints, you can define a Int_as_OT functor as follow:

Module Int_as_OT(I:Int) <: OrderedType.

 Import I.
 Definition t := int.
 Definition eq x y := eq (i2z x) (i2z y).
 Definition lt x y := (Zlt (I.i2z x) (I.i2z y)).

 Lemma eq_refl : forall x : t, eq x x.
   intros;reflexivity.
 Qed.

 Lemma eq_sym : forall x y : t, eq x y -> eq y x.
   symmetry.
   assumption.
 Qed.

 Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
   intros.
   unfold eq in *.
   rewrite H.
   assumption.
 Qed.

 Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
   intros.
   unfold lt in *.
   apply Z_as_OT.lt_trans with (I.i2z y);auto.
 Qed.
  
  
 Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
   intros.
   unfold lt in *.
   apply @Z_as_OT.lt_not_eq.
   assumption.
 Qed.

 Lemma compare : forall x y : t, Compare lt eq x y.
   intros;destruct Z_as_OT.compare with (i2z x) (i2z y).
   apply LT;auto.
   apply EQ;auto.
   apply GT;auto.
 Qed.

 Lemma eq_dec: forall x y:t, {eq x y}+{~ eq x y}.
   intros x y.
   unfold eq.
   do 2 decide equality.
 Qed.

End Int_as_OT.

Module Zint := Z_as_Int.
Module OrderedInt := Int_as_OT( Zint).
Module IMap1 := FMapAVL.Make(OrderedInt).


Ashish Darbari wrote:
> I'm having problems able to use the FMapAVL.
> It works out quite fine if I want the keys 
> to have the type z (IMap), but since I want to use
> this map in ocaml extracted code where keys
> will be ocaml integers, I want to define the
> equivalent module (IMap1) in Coq on Ints, but
> when I do it as shown below, I get an error,
> No such label lt. 
>
> What am I missing?
>
> Thanks
> Ashish
>
> Require Import ZArith.
> Require Import OrderedType.
> Require Import OrderedTypeEx.
> Require Import FMapAVL.
> Require Import Int.
>
>
> Module IMap := FMapAVL.Make(Z_as_OT).
>
> Module IMap1 := FMapAVL.Make(Z_as_Int).