The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

On Mon, 24 Apr 2006 20:08:01 -0500 mulhern 
<mulhern AT gmail.com>
 wrote:

> Theorem name : <goal>.
> Proof.
> <lots of tactics>.
> Qed.

First if you want your proof term to be transparent (ie unfoldable),
you have to finish your proof by "Defined" instead of Qed or Save.


> Definition name_reduced := Eval cbv zeta in name.

This is the right idea but you have to tell cbv to unfold names (delta
reduction). You can try this first:

Definition name_reduced := Eval cbv zeta delta in name.

but this may give to much unfolding. You can focus the delta reduction by 
this:

Definition name_reduced := Eval cbv zeta delta [name_reduced] in name.

This should do the work. [..] can contain a space separated list of
constant names.

Hope this helps.

Pierre Courtieu

> 

> The problem with that is that I can't tell what the body of
> name_reduced consists of because I cannot Print it. When I use the
> Print command I just get
> name_reduced
> =
> name : goal