Nuprl Definition : funtype
funtype(n;A;T) == primrec(n;T;λi,t. ((A (n - 1 - i)) ⟶ t))
Definitions occuring in Statement :
primrec: primrec(n;b;c),
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
primrec: primrec(n;b;c),
lambda: λx.A[x],
function: x:A ⟶ B[x],
apply: f a,
subtract: n - m,
natural_number: $n
FDL editor aliases :
funtype
Latex:
funtype(n;A;T) == primrec(n;T;\mlambda{}i,t. ((A (n - 1 - i)) {}\mrightarrow{} t))
Date html generated:
2016_05_15-PM-02_09_01
Last ObjectModification:
2015_09_23-AM-07_38_02
Theory : untyped!computation
Home
Index