Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] {|...|} Notation (was: Making universe inconsistency only using "Require")

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] {|...|} Notation (was: Making universe inconsistency only using "Require")


chronological Thread 
  • From: AUGER <Cedric.Auger AT lri.fr>
  • To: "Vladimir Voevodsky" <vladimir AT ias.edu>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] {|...|} Notation (was: Making universe inconsistency only using "Require")
  • Date: Thu, 21 Jan 2010 13:35:54 +0100
  • Organization: ProVal

Le Tue, 19 Jan 2010 15:13:47 +0100, Vladimir Voevodsky <vladimir AT ias.edu> a écrit:


PS What is {| ... |} ?? I think the meaning is clear but where is it described in the manual?

On Jan 19, 2010, at 8:32 AM, AUGER wrote:


The {| ... |} notation is the one for records, it is not clearly described in the manual.
I don't know what Coq versions are compatible with.
8.2 works with it to define a record, but you can't pattern match against it,
 and records are never printed this way.
If you define:

Record typed_elt : Type :=
{ T: Type;
  elt: T
}.

then

Definition One := {|T := nat; elt := 1|}.

when you perform

Print One.

You read something like:

One = Build_typed_elt nat 1
    : typed_elt

In the trunk version things are a little better
 as you can use pattern matching and printing is now ok:


One = {| T := nat; elt := 1 |}
     : typed_elt

that is mainly the reason why this notation is not documented

Note that in trunk version you can also use dot notations in record definitions
with {|...|} as:
----------------------------
(*reclogic.v*)
(* this is a funny redefinition of the and predicate automatically
   defining projections *)
Record And (A B: Prop) :=
Conj {Proj1: A; Proj2: B}.

Record Sig (A: Type) (P: A -> Prop): Prop :=
{ witness: A;
  proof: P witness
}.
----------------------------
(*test.v*)
Require reclogic.

Definition true_and_true :=
{|reclogic.Proj1 := I;
  reclogic.Proj2 := I|}.

Goal forall A B, reclogic.And A B -> A.
 Proof.
  intros A B conjunction_of_A_and_B.
  exact (conjunction_of_A_and_B.(reclogic.Proj1)).
 Qed.
-----------------------------
something you can't do in 8.2 without importing the module.

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay




Archive powered by MhonArc 2.6.16.

Top of Page