coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Programming with finite sets, maps, relations

From: Marco Servetto <marco.servetto AT gmail.com>
To: Cedric Auger <sedrikov AT gmail.com>
Cc: Kevin Sullivan <sullivan.kevinj AT gmail.com>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Programming with finite sets, maps, relations
Date: Sat, 3 Aug 2013 08:14:35 +1200

> Definition map (key : Type) (value : Type) := key -> option value.
> Definition empty_map (key : Type) (value : Type) : map key value
> := fun _ => None.
> Definition add (key : Type) (eq_key : forall x y : key, {x=y}+{x<>y}) (value
> : Type)
> (m : map key value) (k : key) (v : value) : map key value
> := fun k' => if eq_key k k' then (Some v) else m k'.

This definition does not enforce the map to be finite, right?

[Coq-Club] Programming with finite sets, maps, relations, Kevin Sullivan, 08/02/2013
- Re: [Coq-Club] Programming with finite sets, maps, relations, Cedric Auger, 08/02/2013
  - Re: [Coq-Club] Programming with finite sets, maps, relations, Kevin Sullivan, 08/02/2013
    - Re: [Coq-Club] Programming with finite sets, maps, relations, Frédéric Blanqui, 08/03/2013
  - Re: [Coq-Club] Programming with finite sets, maps, relations, Marco Servetto, 08/02/2013
- Re: [Coq-Club] Programming with finite sets, maps, relations, Kristopher Micinski, 08/02/2013