Skip to Content.
Sympa Menu

coq-club - [Coq-Club] A question about pattern matching

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A question about pattern matching


chronological Thread 
  • From: geng chen <chengeng4001 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] A question about pattern matching
  • Date: Fri, 22 Jan 2010 22:41:13 +0800
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=wSTtmUDA4q6rXVfZPNeBaS9y/C2jLEyPfi3CheJR/ZVzNC66eN/6ZzluW3f1EyUrbd /vPKgbdxrfMENd5Wd5k6JWmwAeWlogaFBYlLum7AUA0jkRFyM+l9SQ6Z3JLYglqPc0Gv Aq+EOi0/fclWEl5+3e8Jc1QF/hRa6UTRBkoHc=

Hi, everyone.
  I've met a problem about pattern matching. for example there is a function:

Definition check_a (a : nat) : bool :=
match  a  with
  1 => true
  | _ => false
end.

and result of check_a is "true". So how can I prove that a = 1 ?
It is important for me. Could any one help me?
                                                         
Best regards,
Chen



Archive powered by MhonArc 2.6.16.

Top of Page