Nuprl Definition : len

len(as) ==  rec-case(as) of [] => 0 | a::bs => lenbs.lenbs + 1


Definitions occuring in Statement :  list_ind: list_ind,  add: n + m,  natural_number: $n
Definitions occuring in definition :  list_ind: list_ind,  add: n + m,  natural_number: $n
FDL editor aliases :  len
Latex:
len(as)  ==    rec-case(as)  of  []  =>  0  |  a::bs  =>  lenbs.lenbs  +  1


Date html generated: 2016_05_14-AM-07_40_56
Last ObjectModification: 2015_09_22-PM-05_53_55

Theory : list_1


Home Index