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
- [Coq-Club] Why do we need modules anyway?, Chris Dams
- Re: [Coq-Club] Why do we need modules anyway?,
Adam Chlipala
- Re: [Coq-Club] Why do we need modules anyway?,
Stéphane Lescuyer
- Re: [Coq-Club] Why do we need modules anyway?, Chris Dams
- Re: [Coq-Club] Why do we need modules anyway?,
AUGER
- Re: [Coq-Club] Why do we need modules anyway?,
Roman Beslik
- Re: [Coq-Club] Why do we need modules anyway?, Stéphane Lescuyer
- Re: [Coq-Club] Why do we need modules anyway?,
Bas Spitters
- [Coq-Club] Making universe inconsistency only using "Require",
AUGER
- Re: [Coq-Club] Making universe inconsistency only using "Require",
Vladimir Voevodsky
- Re: [Coq-Club] {|...|} Notation (was: Making universe inconsistency only using "Require"), AUGER
- Re: [Coq-Club] Making universe inconsistency only using "Require", roconnor
- Re: [Coq-Club] Making universe inconsistency only using "Require",
Vladimir Voevodsky
- [Coq-Club] Making universe inconsistency only using "Require",
AUGER
- Re: [Coq-Club] Why do we need modules anyway?,
Roman Beslik
- Re: [Coq-Club] Why do we need modules anyway?,
Stéphane Lescuyer
- Re: [Coq-Club] Why do we need modules anyway?,
Adam Chlipala
Archive powered by MhonArc 2.6.16.