Function resolution_prover::implies

pub fn implies(a: Proposition, b: Proposition) -> Proposition

Creates a proposition that is the implication consisting of the two given propositions as the antecedent and consequent repsectively.

let p = resolution_prover::term("p".to_string());
let q = resolution_prover::term("q".to_string());

let p_implies_q = resolution_prover::implies(p, q);

let expected = "p -> q";

assert_eq!(p_implies_q.to_string(), expected);