CurryInfo: contract-prover-4.0.0 / ContractProver.postCondExpOf

definition: Info
 
postCondExpOf :: VerifyInfo -> QName -> [(Int,TypeExpr)] -> TransStateM Term
postCondExpOf ti qf args =
  maybe (return tTrue)
        (\fd -> applyFunc fd args >>= pred2smt)
        (find (\fd -> decodeContractQName (funcName fd)
                        == toPostCondQName (fromNoCheckQName qf))
              (postConds ti))
demand: Info
 no demanded arguments
deterministic: Info
 deterministic operation
documentation: Info
 
Returns the postcondition expression for a given operation
and its arguments (which are assumed to be variable indices).
Rename all local variables by adding `freshvar` to them and
return the new freshvar value.
failfree: Info
 <FAILING>
indeterministic: Info
 referentially transparent operation
infix: Info
 no fixity defined
iotype: Info
 {(_,_,_) |-> _}
name: Info
 postCondExpOf
precedence: Info
 no precedence defined
result-values: Info
 _
signature: Info
 VerifierState.VerifyInfo -> (String, String)
-> [(Prelude.Int, FlatCurry.Types.TypeExpr)]
-> Control.Monad.Trans.State.StateT TransState Prelude.IO ESMT.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