The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The answer to the question of parametricity is that type class resolution is done at type *inference* time, not type *checking* time.  Thus, like notations and the tactics-in-terms of trunk, it has no impact on parametricity.  (Another way of seeing this is that typeclasses live outside the kernel, like tactics and notations.)

-Jason

On Dec 22, 2014 12:30 PM, "Jonathan Leivent" <jonikelee AT gmail.com> wrote:

On 12/22/2014 12:12 PM, Amin Timany wrote:

...
In gallina, you can use the following command:

Definition x := Eval tac in y.

Where tac is a computation tactic, e.g., simpl, cbv, compute, etc. Unfortunately, this construction is only at the level of gallina and not terms. So,

Definition x := z (Eval tac in y).

will generate a parsing error!

But you can do this:

Ltac reduce term :=
  let x := eval compute in term in exact x.

Variable P : nat -> Prop.

Definition foo := P (1+2+3).
Print foo. (* P (1 + 2 + 3) *)

Definition bar := P $(reduce (1+2+3))$.
Print bar. (* P 6 *)

-- Jonathan