Nuprl Definition : omral_alg
omral_alg(g;r) == <|omral(g;r)|, =b, λx,y. tt, λx,y. (x ++ y), 00g,r, λx.(--x), λx,y. (x ** y), 11, λx,y. (inr ⋅ ), λa,\000Cx. (a ⋅⋅ x)>
Definitions occuring in Statement :
omral_minus: --ps
,
omral_zero: 00g,r
,
omral_plus: ps ++ qs
,
omralist: omral(g;r)
,
btrue: tt
,
it: ⋅
,
lambda: λx.A[x]
,
pair: <a, b>
,
inr: inr x
,
set_eq: =b
,
set_car: |p|
Definitions occuring in definition :
set_car: |p|
,
set_eq: =b
,
omralist: omral(g;r)
,
btrue: tt
,
omral_plus: ps ++ qs
,
omral_zero: 00g,r
,
omral_minus: --ps
,
pair: <a, b>
,
inr: inr x
,
it: ⋅
,
lambda: λx.A[x]
Latex:
omral\_alg(g;r) ==
<|omral(g;r)|, =\msubb{}, \mlambda{}x,y. tt, \mlambda{}x,y. (x ++ y), 00g,r, \mlambda{}x.(--x), \mlambda{}x,y. (x ** y), 11, \mlambda{}x,y. (inr \mcdot{} ), \000C\mlambda{}a,x. (a \mcdot{}\mcdot{} x)>
Date html generated:
2016_05_16-AM-08_24_20
Last ObjectModification:
2015_09_23-AM-09_53_17
Theory : polynom_3
Home
Index