CurryInfo: contract-prover-4.0.0 / VerifierState.makeVerifyInfo

definition: Info
 
makeVerifyInfo :: Options -> [AFuncDecl TypeExpr] -> VerifyInfo
makeVerifyInfo opts fdecls = VerifyInfo opts fdecls preconds postconds
 where
  -- Precondition operations:
  preconds  = filter (isPreCondName  . snd . funcName) fdecls
  -- Postcondition operations:
  postconds = filter (isPostCondName . snd . funcName) fdecls
demand: Info
 no demanded arguments
deterministic: Info
 deterministic operation
failfree: Info
 (_, _)
indeterministic: Info
 referentially transparent operation
infix: Info
 no fixity defined
iotype: Info
 {(_,_) |-> {VerifyInfo}}
name: Info
 makeVerifyInfo
precedence: Info
 no precedence defined
result-values: Info
 {VerifyInfo}
signature: Info
 ToolOptions.Options
-> [FlatCurry.Annotated.Types.AFuncDecl FlatCurry.Types.TypeExpr] -> VerifyInfo
solution-complete: Info
 operation might suspend on free variables
terminating: Info
 possibly non-terminating
totally-defined: Info
 reducible on all ground data terms