CurryInfo: property-prover-2.0.0 / Common.postCondExpOf

definition: Info
 
postCondExpOf :: QName -> [(Int,TypeExpr)]
              -> TransStateM SMT.Term
postCondExpOf qf args = do
  postconds <- lift $ gets $ postConds . trInfo
  maybe (return true)
        (\fd -> applyFunc fd args >>= pred2SMT)
        (find (\fd -> decodeContractQName (funcName fd)
                        == toPostCondQName (fromNoCheckQName qf)) postconds)
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
 (String, String) -> [(Prelude.Int, FlatCurry.Types.TypeExpr)]
-> Control.Monad.Trans.State.StateT TransState.TransState (Control.Monad.Trans.State.StateT VerifierState.VState Prelude.IO) Language.SMTLIB.Types.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