The Coq mailing list

[Coq User <coquser AT googlemail.com>]

Can an option Type be between its regular type?

Require Import String.
Require Import List.
Require Import Relation_Definitions.
Record Lane:= {number:nat}.
Record OptionalLane:= {lane:option Lane}.
Record RaceTrack:={tracks:list Lane}.

Definition aLane := (Build_Lane 1).
Definition race := (Build_RaceTrack (aLane::nil)).
Definition optionalLane := Build_OptionalLane aLane. (*Error.  Can 'aLane' be converted to option Lane here?*)
(*Error: The term "aLane" has type "Lane" while it is expected to have type
 "option Lane".*)

On Tue, Aug 18, 2009 at 3:17 AM, <roconnor AT theorem.ca> wrote:

On Mon, 17 Aug 2009, Coq User wrote:

How can I initial a Race with a 'null' laneTwo?  Also how might I test for 'null' given an instance of the
Race record.

Require Import String.
Record Sprinter := {name:string}.
Record Track := {laneOne:Sprinter;laneTwo:Sprinter}.

Definition Race:Track := (Build_Track (Build_Sprinter "Fast") (null??)).

You cannot without explicitly using something like the option type:

Record Track := {laneOne:option Sprinter;laneTwo:option Sprinter}.

Definition Race:Track := (Build_Track (Some (Build_Sprinter "Fast")) None).

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''