Nuprl Definition : egyptian
egyptian(q) ==  norm-pair(λx.x;norm-list(λx.x)) (TERMOF{egyptian-number:o, 1:l} q)
Definitions occuring in Statement : 
norm-list: norm-list(N)
, 
norm-pair: norm-pair(Na;Nb)
, 
apply: f a
, 
lambda: λx.A[x]
Definitions occuring in definition : 
norm-pair: norm-pair(Na;Nb)
, 
norm-list: norm-list(N)
, 
lambda: λx.A[x]
, 
apply: f a
TermOfs occuring in Definition : 
egyptian-number
FDL editor aliases : 
egyptian
Latex:
egyptian(q)  ==    norm-pair(\mlambda{}x.x;norm-list(\mlambda{}x.x))  (TERMOF\{egyptian-number:o,  1:l\}  q)
Date html generated:
2016_05_15-PM-11_43_52
Last ObjectModification:
2015_09_23-AM-08_31_24
Theory : rationals
Home
Index