Nuprl Definition : diff

as bs ==  diff,as,bs. case bs of [] => as b::bs' => diff (as b) bs' esac) as bs

Definitions occuring in Statement :  remove1: as a list_ind: list_ind ycomb: Y apply: a lambda: λx.A[x]
Definitions occuring in definition :  ycomb: Y lambda: λx.A[x] list_ind: list_ind apply: a remove1: as a

as  -  bs  ==    Y  (\mlambda{}diff,as,bs.  case  bs  of  []  =>  as  |  b::bs'  =>  diff  (as  \mbackslash{}  b)  bs'  esac)  as  bs

Date html generated: 2016_05_16-AM-07_39_59
Last ObjectModification: 2015_09_23-AM-09_51_41

Theory : list_2

Home Index