coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] Question on 8.5 primitive projections
- Date: Fri, 30 Jan 2015 12:34:03 +0000
- Accept-language: de-DE, en-US
Dear Matthieu,
I see. I thought they are primitive in the sense that they can just be beta reduced to the record field value, but not delta reduced to a let term. Let me see if Set Printing Projections and/or more careful evaluation solves the readability issues I have in proofs with larger records.
Thanks & best regards,
Michael
From: matthieu.sozeau AT gmail.com [mailto:matthieu.sozeau AT gmail.com]
On Behalf Of Matthieu Sozeau
Hi Michael,
Primitive projections still obey the same reduction rules: delta to unfold it and beta/iota to reduce it, hence they have the unfolded form you witness. However simpl/cbn can recognize them easily and shouldn't ever expose this unfolded
form unless you specifically do a delta reduction. Internally though, the projections are different terms and what you're seeing at the user level just hides the internal representation for compatibility. Also, you may want to Set Printing Projections. -- Matthieu
Dear Coq users,
|
- [Coq-Club] Question on 8.5 primitive projections, Soegtrop, Michael, 01/30/2015
- Re: [Coq-Club] Question on 8.5 primitive projections, Matthieu Sozeau, 01/30/2015
- RE: [Coq-Club] Question on 8.5 primitive projections, Soegtrop, Michael, 01/30/2015
- Re: [Coq-Club] Question on 8.5 primitive projections, Matthieu Sozeau, 01/30/2015
Archive powered by MHonArc 2.6.18.