CurryInfo: verify-non-fail-2.0.0 / Verify.WithSMT.allVarsInTerm

definition: Info 
 
allVarsInTerm :: Term -> [SVar]
allVarsInTerm (TConst _)      = []
allVarsInTerm (TSVar v)       = [v]
allVarsInTerm (TComb _ args)  = foldr union [] (map allVarsInTerm args)
allVarsInTerm (Forall vs arg) = union (map varOfSV vs) (allVarsInTerm arg)
allVarsInTerm (Exists vs arg) = union (map varOfSV vs) (allVarsInTerm arg)
allVarsInTerm (SMT.Let bs e)  =
  foldr union (map fst bs) (map allVarsInTerm (e : map snd bs))
allVarsInTerm (Match e ps)    =
  foldr union [] (map allVarsInTerm (e : map snd ps) ++ map (patVars . fst) ps)
 where
  patVars (PComb _ vs) = vs
demand: Info 
 argument 1
deterministic: Info 
 deterministic operation
documentation: Info 
 
All variables occurring in a SMT term.
failfree: Info 
 _
indeterministic: Info 
 referentially transparent operation
infix: Info 
 no fixity defined
iotype: Info 
 {({TConst}) |-> {[]} || ({TSVar}) |-> {:} || ({TComb}) |-> _ || ({Forall}) |-> _ || ({Exists}) |-> _ || ({Let}) |-> _ || ({Match}) |-> _}
name: Info 
 allVarsInTerm
precedence: Info 
 no precedence defined
result-values: Info 
 _
signature: Info 
 Verify.ESMT.Term -> [Prelude.Int]
solution-complete: Info 
 operation might suspend on free variables
terminating: Info 
 possibly non-terminating
totally-defined: Info 
 reducible on all ground data terms