The Coq mailing list

[roconnor AT theorem.ca]

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.''