property::implies -- test
whether one property implies another
Introductionproperty::implies(prop_1, prop_2) tries to
decide whether prop_1 implies prop_2 or its
converse.
Call(s)property::implies(prop_1, prop_2)
Parametersprop_1, prop_2 |
- | any properties |
ReturnsTRUE, FALSE, or UNKNOWN
Related
Functionsis, assume, property::simpex, bool
Detailsproperty for an overview of all properties.TRUE if prop_2 can be
inferred from prop_1, and FALSE if not prop_2 can
be inferred from prop_1. The result is UNKNOWN if neither implication could
be proved; this may be because neither holds, or because the property
mechanism is too weak to find a proof.
Example
1Every positive integer is positive:
>> property::implies(Type::PosInt, Type::Positive)
TRUE
Some positive numbers are positive integers, and some are not:
>> property::implies(Type::Positive, Type::PosInt)
UNKNOWN
No positive number is a negative integer:
>> property::implies(Type::Positive, Type::NegInt)
FALSE