The Coq mailing list

[Damien Pous <Damien.Pous AT inria.fr>]

Hi,

You are almost done : it suffices to use the functions provided by
your NatMap module.
It's interface is given here :
http://coq.inria.fr/stdlib/Coq.FSets.FMapInterface.html
For instance, you can write :

Definition m := NatMap.add 1 2 (NatMap.add 2 3 (@NatMap.empty nat)).
Compute NatMap.get 2 m.

Lemmas about finite maps can be used in the same way, using the
"NatMap.foo" notation.

Damien

2011/11/8  
<darvishdarab AT gmail.com>:
> Hi everyone,
>
> I am a newbie to Coq and I've got a question that I don't  really think is 
> hard
> to answer but I spent some time on it with no luck and I couldn't find any
> examples online, so I thought I just ask it here:
>
> I have the following:
>
> Require Import FMaps.
> Require Import Arith.
>
> Module NatOrd <: OrderedType.
> ...
> End NatOrd.
>
> and then I define:
>
> Definition NatMap := FMapList.Make (NatOrd).
>
> and:
>
> Definition NatNatMap := NatMap.t nat.
>
> My question is that how I can work with this NatNatMap. I don't know how to
> actually define something that has type NatMap.t nat and I can add/remove/..
> elements to it. What I basically want to do is to define a partial map from
> naturals to some other type. What are the possibly ways one can do this in 
> Coq?
>
> Thank you in advance for your help.
>