diff --git a/src/format.rs b/src/format.rs
index c6b8896..26c0a77 100644
--- a/src/format.rs
+++ b/src/format.rs
@@ -66,6 +66,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
+		{
+			crate::ImplicationDirection::LeftToRight => write!(format, "left to right"),
+			crate::ImplicationDirection::RightToLeft => write!(format, "right to left"),
+		}
+	}
+}
+
 impl std::fmt::Debug for crate::SpecialInteger
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
@@ -391,14 +403,15 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 			},
 			crate::Formula::Implies(crate::Implies{direction, antecedent, implication}) =>
 			{
-				let operator_symbol = match direction
+				match direction
 				{
-					crate::ImplicationDirection::LeftToRight => "->",
-					crate::ImplicationDirection::RightToLeft => "<-",
+					crate::ImplicationDirection::LeftToRight =>
+						write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence),
+							display_formula(implication, precedence))?,
+					crate::ImplicationDirection::RightToLeft =>
+						write!(format, "{:?} <- {:?}", display_formula(implication, precedence),
+							display_formula(antecedent, precedence))?,
 				};
-
-				write!(format, "{:?} {} {:?}", display_formula(antecedent, precedence),
-					operator_symbol, display_formula(implication, precedence))?;
 			},
 			crate::Formula::IfAndOnlyIf(arguments) =>
 			{
diff --git a/src/parse/formulas.rs b/src/parse/formulas.rs
index b13bb57..a1d287e 100644
--- a/src/parse/formulas.rs
+++ b/src/parse/formulas.rs
@@ -131,7 +131,7 @@ fn or<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formu
 	)(i)
 }
 
-fn implication_left_to_right<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
+fn implies_left_to_right<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	map
 	(
@@ -155,11 +155,11 @@ fn implication_left_to_right<'a>(i: &'a str, d: &Declarations) -> IResult<&'a st
 		|(arguments, last_argument)| arguments.into_iter().rev().fold(last_argument,
 			|accumulator, argument|
 				crate::Formula::implies(crate::ImplicationDirection::LeftToRight,
-					Box::new(accumulator), Box::new(argument)))
+					Box::new(argument), Box::new(accumulator)))
 	)(i)
 }
 
-fn implication_right_to_left<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
+fn implies_right_to_left<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
 {
 	map
 	(
@@ -183,7 +183,7 @@ fn implication_right_to_left<'a>(i: &'a str, d: &Declarations) -> IResult<&'a st
 		|(first_argument, arguments)| arguments.into_iter().fold(first_argument,
 			|accumulator, argument|
 				crate::Formula::implies(crate::ImplicationDirection::RightToLeft,
-					Box::new(accumulator), Box::new(argument)))
+					Box::new(argument), Box::new(accumulator)))
 	)(i)
 }
 
@@ -264,7 +264,7 @@ where
 
 				d.variable_declaration_stack.borrow_mut().push(std::rc::Rc::clone(&variable_declarations));
 
-				let (i, argument) = formula_parenthesized(i, d)?;
+				let (i, argument) = formula_precedence_0(i, d)?;
 
 				// TODO: report logic errors more appropriately
 				d.variable_declaration_stack.borrow_mut().pop()
@@ -438,8 +438,8 @@ fn formula_precedence_5<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, cr
 {
 	alt
 	((
-		|i| implication_left_to_right(i, d),
-		|i| implication_right_to_left(i, d),
+		|i| implies_left_to_right(i, d),
+		|i| implies_right_to_left(i, d),
 		|i| formula_precedence_4(i, d),
 	))(i)
 }