Nuprl Definition : fun_exp
f^n ==  primrec(n;λx.x;λi,g. (f o g))
Definitions occuring in Statement : 
compose: f o g
, 
primrec: primrec(n;b;c)
, 
lambda: λx.A[x]
Definitions occuring in definition : 
primrec: primrec(n;b;c)
, 
lambda: λx.A[x]
, 
compose: f o g
Rules referencing : 
compactness, 
fixpointLeast
FDL editor aliases : 
fun_exp
Latex:
f\^{}n  ==    primrec(n;\mlambda{}x.x;\mlambda{}i,g.  (f  o  g))
Date html generated:
2016_05_13-PM-04_06_15
Last ObjectModification:
2015_09_22-PM-05_45_51
Theory : fun_1
Home
Index