Macro cvlr_implies 

macro_rules! cvlr_implies {
    ($a:expr, $b:expr) => { ... };
}

Creates a boolean expression representing logical implication (A → B).

This macro is a convenience wrapper around cvlr_implies that provides flexible syntax for creating implications. It supports both identifiers and expressions as arguments.

An implication A → B evaluates to true when either:

• The antecedent A is false, or
• Both A and B are true

Syntax

cvlr_implies!(antecedent, consequent)

Arguments

• antecedent - The left-hand side (A) of the implication, can be an identifier or expression
• consequent - The right-hand side (B) of the implication, can be an identifier or expression

Both arguments must implement CvlrFormula with the same context type.

Returns

Returns a value implementing CvlrFormula that represents the logical implication antecedent → consequent.

Examples

use cvlr_spec::{cvlr_implies, cvlr_predicate, CvlrFormula};

struct Counter {
    value: i32,
}

// Using identifiers
cvlr_def_predicate! {
    pred IsPositive(c: Counter) {
        c.value > 0
    }
}

cvlr_def_predicate! {
    pred IsEven(c: Counter) {
        c.value % 2 == 0
    }
}

let ctx1 = Counter { value: 6 };
let expr = cvlr_implies!(IsPositive, IsEven);
assert!(expr.eval(&ctx1)); // 6 > 0 → 6 % 2 == 0 (both true, so true)

let ctx2 = Counter { value: 5 };
assert!(!expr.eval(&ctx2)); // 5 > 0 → 5 % 2 == 0 (antecedent true, consequent false, so false)

let ctx3 = Counter { value: -2 };
assert!(expr.eval(&ctx3)); // -2 > 0 → ... (antecedent false, so true)

// Using expressions
let expr2 = cvlr_implies!(
    cvlr_predicate! { | c : Counter | -> { c.value > 0 } },
    cvlr_predicate! { | c : Counter | -> { c.value < 100 } }
);
assert!(expr2.eval(&ctx1));

// Mixed identifiers and expressions
let expr3 = cvlr_implies!(
    IsPositive,
    cvlr_predicate! { | c : Counter | -> { c.value < 100 } }
);
assert!(expr3.eval(&ctx1));