CurryInfo: contract-prover-4.0.0 / ESMT.substTerm

definition: Info 
 
substTerm :: TPSubst -> Term -> Term
substTerm sub term = case term of
  TConst _ -> term
  TSVar  _ -> term
  TComb f args -> TComb (substQId sub f) (map (substTerm sub) args)
  Forall svs arg -> Forall (map (substSV sub) svs) (substTerm sub arg)
  Exists svs arg -> Forall (map (substSV sub) svs) (substTerm sub arg)
  Let bs e -> Let (map (\ (v,s) -> (v, substTerm sub s)) bs) (substTerm sub e)
demand: Info 
 argument 2
deterministic: Info 
 deterministic operation
documentation: Info 
 
Applies a sort substitution to a term.
failfree: Info 
 (_, _)
indeterministic: Info 
 referentially transparent operation
infix: Info 
 no fixity defined
iotype: Info 
 {(_,{TConst}) |-> {TConst} || (_,{TSVar}) |-> {TSVar} || (_,{TComb}) |-> {TComb} || (_,{Forall}) |-> {Forall} || (_,{Exists}) |-> {Forall} || (_,{Let}) |-> {Let}}
name: Info 
 substTerm
precedence: Info 
 no precedence defined
result-values: Info 
 _
signature: Info 
 Data.Map.Map String Sort -> Term -> Term
solution-complete: Info 
 operation might suspend on free variables
terminating: Info 
 possibly non-terminating
totally-defined: Info 
 possibly non-reducible on same data term