The Coq mailing list

[Larry Lee <llee454 AT gmail.com>]

Is it possible to simplify fixed point expressions over non-constant arguments?

The Eval command and the lazy and cbv tactics can be used to simplify these expressions over constants. For example:

    Eval lazy iota in ((fix f (x : nat) := if eq_nat_dec x 0 then true else false) 1).

evaluates to

    (fun (x : nat) => if eq_nat_dec x 0 then true else false) 1.

but

    Eval lazy iota in ((fix f (x : nat) := if eq_nat_dec x 0 then true else false) y).

should evaluate to

    (fun (x : nat) => if eq_nat_dec x 0 then true else false) y

but does not simplify at all.

Is there something that I'm missing?

Thanks,
Larry