The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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.
Best,

-- Matthieu

Le vendredi 30 janvier 2015, Soegtrop, Michael <michael.soegtrop AT intel.com> a écrit :

Dear Coq users,

I really like the primitive projections feature, because the let terms to which projections expand sometimes make proof contexts with large records hard to understand. Just it doesn't work as I expected.

In the below sample:

        Set Primitive Projections.

        Record Test :=
        {
          a : unit;
          b : bool;
          c : nat
        }.

        Print a.

I get

        a = fun t : Test => let (a, _, _) := t in a : Test -> unit

I expected that the let term would go away and be replaced by the new primitive projection term. Also if I try

        Definition test := Build_Test tt false 0.
        Definition testa := test.(a).
        Eval cbv delta beta in testa.

I get

     = let (a, _, _) := {| a := tt; b := false; c := 0 |} in a
     : unit

I used the 8.5beta1 windows version.

Best regards,

Michael

--