coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Empty Record Field

From: Coq User <coquser AT googlemail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Empty Record Field
Date: Mon, 17 Aug 2009 21:48:56 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=EyhphyOv9eetOHkizv2VAb4rsx8Oem3VRSgjFWq97yM3Bcv/US7wofbVR2aDwbryGX LhArqE3C44Y/CT6KN+x+jS4SihusY2zIVk24ozgeQjtU1GtF8KsArfVBVY+SLwbl1gjC CUPeFCDqLFfP5cb/rn4J1k2CqGW/QeLHmBtFI=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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??)).

[Coq-Club] Empty Record Field, Coq User
- Re: [Coq-Club] Empty Record Field, roconnor
  - Re: [Coq-Club] Empty Record Field, Coq User