coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Two options in the Coq Standard Library

From: Steve Zdancewic <stevez AT cis.upenn.edu>
To: coq-club AT pauillac.inria.fr
Cc: Study group on Mechanized Metatheory for the Masses <provers AT lists.seas.upenn.edu>
Subject: [Coq-Club] Two options in the Coq Standard Library
Date: Thu, 10 Feb 2005 10:47:33 -0500
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi everyone,

Is there a reason why there are two different implementations of options?

Coq.Init.Datatypes has this:

Inductive option (A:Set) : Set :=
  | Some : A -> option A
  | None : option A.

Implicit Arguments None [A].

Most of the library lemmas are about this version of options, and because of the implicit parameter, they're a bit easier to use.

However, Coq.IntMap.Map has this:

Inductive option : Set :=
    | NONE : option
    | SOME : A -> option.

(No implicit argument declaration.)

Having two kinds of options is quite annoying when trying to use the map library with the basic datatypes.

Thanks for your help!

Steve Zdancewic
Dept. of Computer and Information Science
University of Pennsylvania

[Coq-Club] Two options in the Coq Standard Library, Steve Zdancewic