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

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

     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 !