Nuprl Definition : l-ind
l-ind(L;nilcase;h,t,r.F[h; t; r])
==r eval v = L in
if v = Ax then nilcase otherwise let h,t = v
in F[h; t; l-ind(t;nilcase;h,t,r.F[h; t; r])]
l-ind(L;nilcase;h,t,r.F[h; t; r]) ==
fix((λl-ind,L. eval v = L in if v = Ax then nilcase otherwise let h,t = v in F[h; t; l-ind t])) L
Definitions occuring in Statement :
callbyvalue: callbyvalue,
isaxiom: if z = Ax then a otherwise b,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
callbyvalue: callbyvalue,
isaxiom: if z = Ax then a otherwise b,
spread: spread def,
apply: f a
FDL editor aliases :
l-ind
Latex:
l-ind(L;nilcase;h,t,r.F[h; t; r])
==r eval v = L in
if v = Ax then nilcase otherwise let h,t = v
in F[h; t; l-ind(t;nilcase;h,t,r.F[h; t; r])]
Latex:
l-ind(L;nilcase;h,t,r.F[h; t; r]) ==
fix((\mlambda{}l-ind,L. eval v = L in if v = Ax then nilcase otherwise let h,t = v in F[h; t; l-ind t])) L
Date html generated:
2016_05_14-AM-06_26_49
Last ObjectModification:
2015_12_03-PM-02_04_46
Theory : list_0
Home
Index