Le Thu, 8 Sep 2011 16:42:39 +0200 (CEST),
Walter Cazzola cazz...@dico.unimi.it a écrit :
On Thu, 8 Sep 2011, Esther Baruk wrote:
You must also put the signature of the module type CharPQueueAbs in
the implementation (A.ml).
this means that can't I separate signature from the
Hi all,
while playing with coq and extraction I did the following:
Fixpoint narity (n: nat) : Set :=
match n with
| O = nat
| S n = nat - (narity n)
end.
Definition sum_aux : nat - forall n, narity n :=
fix sum acc n :=
match n as n0 return narity n0 with
| O = acc
| S n = fun m = sum
