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