Nuprl Definition : omral_times
ps ** qs == Y (λomral_times,ps. case ps of [] => [] | p::ps' => (<fst(p),snd(p)>* qs) ++ (omral_times ps') esac) ps
Definitions occuring in Statement :
omral_scale: <k,v>* ps
,
omral_plus: ps ++ qs
,
list_ind: list_ind,
nil: []
,
pi1: fst(t)
,
pi2: snd(t)
,
ycomb: Y
,
apply: f a
,
lambda: λx.A[x]
Definitions occuring in definition :
ycomb: Y
,
lambda: λx.A[x]
,
list_ind: list_ind,
nil: []
,
omral_plus: ps ++ qs
,
omral_scale: <k,v>* ps
,
pi1: fst(t)
,
pi2: snd(t)
,
apply: f a
Latex:
ps ** qs ==
Y (\mlambda{}omral$_{times}$,ps. case ps of [] => [] | p::ps' => (<fst(p),snd(p)>* qs) \000C++ (omral$_{times}$ ps') esac) ps
Date html generated:
2016_05_16-AM-08_25_23
Last ObjectModification:
2015_09_23-AM-09_53_18
Theory : polynom_3
Home
Index