The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Dear Vladimir,

It's due to the constructor restriction of fixpoints: a fixpoint is only unfolded when it's structural argument starts with a constructor. Here, Coq infers that the structural argument is n, and since you pass a variable as a first argument in "minuswithzero n O", the reduction is stuck. A fix is to specify the structural argument in the Fixpoint definition:

Fixpoint minuswithzero ( n m : nat ) { struct m } : nat :=
  match m , n with
  | O , n => n
  | S k , O => O
  | S k , S l => minuswithzero l k
  end .

Lemma test ( n : nat ) : paths n ( minuswithzero n O ) .
Proof . intro . unfold minuswithzero . apply idpath .

On 16 December 2013 17:34, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

Hello,

could someone explain to me why the following code does not compile?


Fixpoint minuswithzero ( n m : nat ) : nat :=

match m , n with

| O , n => n
| S k , O => O
| S k , S l => minuswithzero l k
end .

Lemma test ( n : nat ) : paths n ( minuswithzero n O ) .
Proof . intro . unfold minuswithzero . apply idpath .



V.