Function resolution_prover::iff

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

Creates a proposition that is the biconditional of the two given propositions.

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

let p_iff_q = resolution_prover::iff(p, q);

let expected = "p <-> q";

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