The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

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.