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