CurryInfo: contract-prover-4.0.0 / ContractProver.addPostConditionTo

definition:
 
addPostConditionTo :: QName -> TAFuncDecl -> TAFuncDecl
addPostConditionTo pfname fdecl = let fn = funcName fdecl in
  if toPostCondQName fn == pfname
    then updFuncBody (const (addPostConditionCheck fn (funcRule fdecl))) fdecl
    else fdecl
demand:
 argument 1
deterministic:
 deterministic operation
documentation:
 
If the function declaration is the declaration of the given function name,
decorate it with a postcondition check.
failfree:
 <FAILING>
indeterministic:
 referentially transparent operation
infix:
 no fixity defined
iotype:
 {(_,_) |-> _}
name:
 addPostConditionTo
precedence:
 no precedence defined
result-values:
 _
signature:
 (String, String) -> FlatCurry.Annotated.Types.AFuncDecl FlatCurry.Types.TypeExpr
-> FlatCurry.Annotated.Types.AFuncDecl FlatCurry.Types.TypeExpr
solution-complete:
 operation might suspend on free variables
terminating:
 possibly non-terminating
totally-defined:
 possibly non-reducible on same data term