Nuprl Definition : free-vars-aux
free-vars-aux(bnds;t) ==
case t
of inl(v) =>
if v ∈b bnds then [] else [v] fi
| inr(p) =>
let op,bts = p
in l-union-list(VarDeq;map(λbt.let vs,a = bt
in free-vars-aux(rev(vs) + bnds;a);bts))
Definitions occuring in Statement :
var-deq: VarDeq,
l-union-list: l-union-list(eq;ll),
deq-member: x ∈b L,
rev-append: rev(as) + bs,
map: map(f;as),
cons: [a / b],
nil: [],
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
deq-member: x ∈b L,
cons: [a / b],
nil: [],
l-union-list: l-union-list(eq;ll),
var-deq: VarDeq,
map: map(f;as),
lambda: λx.A[x],
spread: spread def,
rev-append: rev(as) + bs
FDL editor aliases :
free-vars-aux
Latex:
free-vars-aux(bnds;t) ==
case t
of inl(v) =>
if v \mmember{}\msubb{} bnds then [] else [v] fi
| inr(p) =>
let op,bts = p
in l-union-list(VarDeq;map(\mlambda{}bt.let vs,a = bt
in free-vars-aux(rev(vs) + bnds;a);bts))
Date html generated:
2020_05_19-PM-09_55_55
Last ObjectModification:
2020_03_09-PM-04_09_08
Theory : terms
Home
Index