Nuprl Definition : diff
as - bs == Y (λ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: f a,
lambda: λx.A[x]
Definitions occuring in definition :
ycomb: Y,
lambda: λx.A[x],
list_ind: list_ind,
apply: f a,
remove1: as \ a
Latex:
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