Nuprl Definition : vars-of-subst
vars-of-subst(s) ==
l-union-list(VarDeq;map(λvt.let v,t = vt
in if eq_var(v;nullvar()) then free-vars(t) else insert(v;free-vars(t)) fi ;s))
Definitions occuring in Statement :
free-vars: free-vars(t),
nullvar: nullvar(),
var-deq: VarDeq,
eq_var: eq_var(a;b),
l-union-list: l-union-list(eq;ll),
insert: insert(a;L),
map: map(f;as),
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
l-union-list: l-union-list(eq;ll),
map: map(f;as),
lambda: λx.A[x],
spread: spread def,
ifthenelse: if b then t else f fi ,
eq_var: eq_var(a;b),
nullvar: nullvar(),
insert: insert(a;L),
var-deq: VarDeq,
free-vars: free-vars(t)
FDL editor aliases :
vars-of-subst
Latex:
vars-of-subst(s) ==
l-union-list(VarDeq;map(\mlambda{}vt.let v,t = vt
in if eq\_var(v;nullvar())
then free-vars(t)
else insert(v;free-vars(t))
fi ;s))
Date html generated:
2020_05_19-PM-09_57_40
Last ObjectModification:
2020_03_09-PM-04_09_55
Theory : terms
Home
Index