On 16/01/13 19:49, Yuntao Peng wrote: > Now there is a goals I want to prove [...]
> Thanks to the listTheory is base on real, so I can not use its theorem. I’m not sure what you mean by this last sentence. Certainly, the theory of lists (listTheory) is not tied to real numbers at all. Also, assuming you don’t use MAP2 as Ramana suggested, you might also prefer to write your definitions like val list_ADD_def = Define` (list_ADD [] _ = []) /\ (list_ADD _ [] = []) /\ (list_ADD ((c1:complex)::t1) (c2::t2) = (c1 + c2) :: list_ADD t1 t2) ` Best, Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS, MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft MVPs and experts. ON SALE this month only -- learn more at: http://p.sf.net/sfu/learnmore_122712
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
