Entry	Value
Package Name	list-length-thm
Count	4
Theorems	LENGTH_EQ_CONS : !l n. LENGTH l = SUC n <=> (?h t. l = CONS h t /\ LENGTH t = n) LENGTH_EQ_NIL : !l. LENGTH l = 0 <=> l = [] LENGTH_TL : !l. ~NULL l ==> LENGTH (TL l) = LENGTH l - 1 NULL_LENGTH : !l. LENGTH l = 0 <=> NULL l

Back to main package page