diff --git a/src/ast.rs b/src/ast.rs
index b75d806..3c60ed2 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -29,6 +29,15 @@ pub enum UnaryOperator
 	Negative,
 }
 
+// ImplicationDirection
+
+#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
+pub enum ImplicationDirection
+{
+	LeftToRight,
+	RightToLeft,
+}
+
 // Primitives
 
 #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
@@ -293,16 +302,19 @@ impl IfAndOnlyIf
 
 pub struct Implies
 {
+	pub direction: ImplicationDirection,
 	pub antecedent: Box<Formula>,
 	pub implication: Box<Formula>,
 }
 
 impl Implies
 {
-	pub fn new(antecedent: Box<Formula>, implication: Box<Formula>) -> Self
+	pub fn new(direction: ImplicationDirection, antecedent: Box<Formula>, implication: Box<Formula>)
+		-> Self
 	{
 		Self
 		{
+			direction,
 			antecedent,
 			implication,
 		}
@@ -524,9 +536,10 @@ impl Formula
 		Self::IfAndOnlyIf(IfAndOnlyIf::new(left, right))
 	}
 
-	pub fn implies(antecedent: Box<Formula>, consequent: Box<Formula>) -> Self
+	pub fn implies(direction: ImplicationDirection, antecedent: Box<Formula>,
+		consequent: Box<Formula>) -> Self
 	{
-		Self::Implies(Implies::new(antecedent, consequent))
+		Self::Implies(Implies::new(direction, antecedent, consequent))
 	}
 
 	pub fn less(left: Box<Term>, right: Box<Term>) -> Self
diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index b5dcfd6..27b644a 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -28,6 +28,18 @@ impl Precedence for crate::Formula
 	}
 }
 
+impl std::fmt::Debug for crate::ImplicationDirection
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match &self
+		{
+			Self::LeftToRight => write!(format, "left to right"),
+			Self::RightToLeft => write!(format, "right to left"),
+		}
+	}
+}
+
 impl std::fmt::Debug for crate::PredicateDeclaration
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
@@ -140,9 +152,14 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 					separator = " or "
 				}
 			},
-			crate::Formula::Implies(crate::Implies{antecedent, implication})
+			crate::Formula::Implies(crate::Implies{
+				direction: crate::ImplicationDirection::LeftToRight, antecedent, implication})
 				=> write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence),
 					display_formula(implication, precedence))?,
+			crate::Formula::Implies(crate::Implies{
+				direction: crate::ImplicationDirection::RightToLeft, antecedent, implication})
+				=> write!(format, "{:?} <- {:?}", display_formula(implication, precedence),
+					display_formula(antecedent, precedence))?,
 			crate::Formula::IfAndOnlyIf(crate::IfAndOnlyIf{left, right})
 				=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence),
 					display_formula(right, precedence))?,