[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] some problems about list which is provided by the prelude



 Hello,
 
     If I use cons(a,cons(b,null) in my file ,I know using length(cons(a,cons(b,null)) can get the length of the list,but  I want to get the length in the prove that is using prover command gets the real value ,2.How could I do?Thank you !
 
 
 



22元超值饭面,8.5折纯珍比萨,必胜宅急送网上点餐优惠多