The Coq mailing list

[zell08v AT orange.fr]

Hello I am a very beginner on Coq.

My first program Coq doesnot work, 
(from a  homewrk of a course of B.Pierce)
anyone can tell me why?

Error Message:
Toplevel input, characters 471-476:
Error: The reference nandb was not found in the current environment.

The programme:
(** This function should return [true] if either or both of
    its inputs are [false]. *)
Definition nandb (b1:bool) (b2:bool) : bool :=  orb (negb b1) (negb b2)
  (*negb and orb is defined earlier as 'negation' and 'or')

(** Remove "[Admitted.]" and fill in each proof with 
    "[Proof. simpl. reflexivity. Qed.]" *)

Example test_nandb1:               (nandb true false) = true.
Proof.simpl.reflexivity.Qud.
...