Nuprl Definition : mrec-ind
mrec-ind(h;o) == let lbl,tpl = o in letrec r(i)=λx.(h <i, x> (λo'.let j,z = o' in r j z)) in r(lbl) tpl
Definitions occuring in Statement :
genrec-ap: genrec-ap,
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>
Definitions occuring in definition :
genrec-ap: genrec-ap,
pair: <a, b>,
lambda: λx.A[x],
spread: spread def,
apply: f a
FDL editor aliases :
mrec-ind
Latex:
mrec-ind(h;o) ==
let lbl,tpl = o
in letrec r(i)=\mlambda{}x.(h <i, x> (\mlambda{}o'.let j,z = o' in r j z)) in r(lbl) tpl
Date html generated:
2019_06_20-PM-02_16_25
Last ObjectModification:
2019_02_28-PM-02_09_44
Theory : tuples
Home
Index