CurryInfo: contract-prover-4.0.0 / ContractProver.axiomatizedOps
definition: 
|
axiomatizedOps :: [String] axiomatizedOps = ["Prelude_null","Prelude_take","Prelude_length"] |
|
demand:
|
no demanded arguments |
|
deterministic:
|
deterministic operation |
|
documentation:
|
Operations axiomatized by specific smt scripts (no longer necessary since these scripts are now automatically generated by Curry2SMT.funcs2SMT). However, for future work, it might be reasonable to cache these scripts for faster contract checking. |
|
failfree:
|
() |
|
indeterministic:
|
referentially transparent operation |
|
infix:
|
no fixity defined |
|
iotype:
|
{() |-> {:}}
|
|
name:
|
axiomatizedOps |
|
precedence:
|
no precedence defined |
|
result-values:
|
{:}
|
|
signature:
|
[String] |
|
solution-complete:
|
operationally complete operation |
|
terminating:
|
yes |
|
totally-defined:
|
reducible on all ground data terms |