The Coq mailing list

[Babak Moazzez <babakmoazzez AT yahoo.com>]

Hi.

I am trying to define a function in Coq that adds two lists together. for this purpose , I need to use a structure which is very familiar in any programming language:

if (p=q) then do ....

but in Coq I cannot use this since (p=q) is not a boolean value but just a proposition which needs to be proved if it is true.

Can anybody tell me what to do?

Thanks.
 

Babak Moazzez
School of Mathematics and Statistics
Carleton University

Address:
Room 4356, Herzberg Building
Carleton University
1125 Colonel By Drive
Ottawa, ON K1S 5B6
Canada

Web: www.math.carleton.ca/~bmoazzez

Tel: 613 520 2600 Ext. 8789
Email: bmoazzez AT math.carleton.ca or babakmoazzez AT yahoo.com

---

  New Email addresses available on Yahoo!  
Get the Email name you've always wanted on the new @ymail and @rocketmail.
Hurry before someone else does!