Nuprl Definition : all-vars

all-vars(t) ==
  case t
   of inl(v) =>
   [v]
   | inr(p) =>
   let op,bts = p
   in accumulate (with value as and list item bt):
       let vs,a = bt
       in all-vars(a) ⋃ vs ⋃ as
      over list:
        bts
      with starting value:
       [])

Definitions occuring in Statement : var-deq: VarDeq, l-union: as ⋃ bs, list_accum: list_accum, cons: [a / b], nil: [], 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], cons: [a / b], list_accum: list_accum, spread: spread def, l-union: as ⋃ bs, var-deq: VarDeq, nil: []
FDL editor aliases : all-vars

Latex:
all-vars(t) == case t of inl(v) => [v] | inr(p) => let op,bts = p in accumulate (with value as and list item bt): let vs,a = bt in all-vars(a) \mcup{} vs \mcup{} as over list: bts with starting value: []) Date html generated: 2020_05_19-PM-09_56_15 Last ObjectModification: 2020_03_09-PM-04_09_16 Theory : terms Home Index