The Coq mailing list

[<michael.soegtrop AT intel.com>]

Dear COQ users,

I wonder if there is a way to specify the recursion depth in simpl or cbv
tactics. E.g. in the following case:

Fixpoint even (n:nat) : Prop :=
  match n with
  | 0 => True
  | 1 => False
  | S (S p) => even p
  end.

Eval simpl in even(4).

is it possible to get even(2) as answer instead of True? This is of cause a
not so interesting example, but I have a case where I want to restrict the
evaluation depth in an inductive proof, because after one evaluation I can use
the induction hypothesis to simplify the goal, but not after full recursive
evalutaion.

Thanks & best regards,

Michael