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