The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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