From 80d7460ec14b2dff1c9d63ea5571cea91aa9a631 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Mon, 6 Apr 2020 21:45:32 +0200
Subject: [PATCH] Start testing implications

---
 src/format/formulas.rs | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index c577fd0..0fc9d9b 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -1673,4 +1673,25 @@ mod tests
 				if_and_only_if(vec![or(p2q2r2())]), if_and_only_if(vec![or(p3q3r3())])])),
 			"p1 or q1 or r1 <-> p2 or q2 or r2 <-> p3 or q3 or r3");
 	}
+
+	#[test]
+	fn format_combination_implies_and_lower()
+	{
+		// Implies + implies
+		assert_eq!(format(
+			implies_right(implies_right(p1(), q1()), implies_right(p2(), q2()))),
+			"(p1 -> q1) -> p2 -> q2");
+		assert_eq!(format(
+			implies_right(and(vec![implies_right(p1(), q1())]),
+				and(vec![implies_right(p2(), q2())]))),
+			"(p1 -> q1) -> p2 -> q2");
+		assert_eq!(format(
+			implies_right(or(vec![implies_right(p1(), q1())]),
+				or(vec![implies_right(p2(), q2())]))),
+			"(p1 -> q1) -> p2 -> q2");
+		assert_eq!(format(
+			implies_right(if_and_only_if(vec![implies_right(p1(), q1())]),
+				if_and_only_if(vec![implies_right(p2(), q2())]))),
+			"(p1 -> q1) -> p2 -> q2");
+	}
 }