The Coq mailing list

[Randy Pollack <rpollack AT seas.harvard.edu>]

I tried the "Function" command for the first time, with a simple
nat-valued measure.

Function psub (P:bbS) (X:PP) (M:bbS) {measure bbS_size M} : bbS :=
  match M with
    | par Y => (if PPeq Y X then P else M)
    | var _ => M
    | app Q N => app (psub P X Q) (psub P X N)
    | lam n N => lam n (psub P X (rename n X N))
  end.

(The point is that [bbS_size (rename n X N)] is the same as [bbS_size N].)

I proved the generated goals without any problem (using "omega").

I want psub to evaluate by computation as if I had defined it by
Fixpoint, but this doesn't seem to work; blocked by "psub_terminate".
By playing around, I found that "psub_F psub" evaluates, but how can I
use this?

I guess there are also propositional equations proved somewhere; is
that how the defined function psub is intended to be used?

Thanks for any help. (I can provide all details, but I don't think
that is central to my question.)

Randy