diff --git a/src/format/formulas.rs b/src/format/formulas.rs
index 0fc9d9b..7cf24d6 100644
--- a/src/format/formulas.rs
+++ b/src/format/formulas.rs
@@ -1,77 +1,5 @@
 use super::*;
 
-fn requires_parentheses<'formula>(formula: &'formula crate::Formula,
-	parent_formula: &'formula crate::Formula)
-	-> bool
-{
-	use crate::Formula;
-
-	match formula
-	{
-		Formula::Predicate(_)
-		| Formula::Boolean(_)
-		| Formula::Compare(_)
-		| Formula::Not(_)
-		| Formula::Exists(_)
-		| Formula::ForAll(_)
-			=> false,
-		Formula::And(formulas)
-		| Formula::Or(formulas)
-		| Formula::IfAndOnlyIf(formulas) if formulas.len() <= 1
-			=> false,
-		Formula::And(_) => match *parent_formula
-		{
-			Formula::Not(_)
-			| Formula::Exists(_)
-			| Formula::ForAll(_)
-				=> true,
-			_ => false,
-		},
-		Formula::Or(_) => match *parent_formula
-		{
-			Formula::Not(_)
-			| Formula::Exists(_)
-			| Formula::ForAll(_)
-			| Formula::And(_)
-				=> true,
-			_ => false,
-		},
-		Formula::Implies(crate::Implies{direction, ..}) => match &*parent_formula
-		{
-			Formula::Not(_)
-			| Formula::Exists(_)
-			| Formula::ForAll(_)
-			| Formula::And(_)
-			| Formula::Or(_)
-				=> true,
-			Formula::Implies(
-				crate::Implies{direction: parent_direction, antecedent: parent_antecedent, ..}) =>
-				if direction == parent_direction
-				{
-					// Implications with the same direction nested on the antecedent side require
-					// parentheses because implication is considered right-associative
-					std::ptr::eq(formula, &**parent_antecedent)
-				}
-				else
-				{
-					true
-				},
-			_ => false,
-		},
-		Formula::IfAndOnlyIf(_) => match *parent_formula
-		{
-			Formula::Not(_)
-			| Formula::Exists(_)
-			| Formula::ForAll(_)
-			| Formula::And(_)
-			| Formula::Or(_)
-			| Formula::Implies(_)
-				=> true,
-			_ => false,
-		},
-	}
-}
-
 impl std::fmt::Debug for crate::ImplicationDirection
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
@@ -106,6 +34,85 @@ struct FormulaDisplay<'formula>
 	parent_formula: Option<&'formula crate::Formula>,
 }
 
+impl<'formula> FormulaDisplay<'formula>
+{
+	fn requires_parentheses(&self) -> bool
+	{
+		use crate::Formula;
+
+		let parent_formula = match self.parent_formula
+		{
+			Some(parent_formula) => parent_formula,
+			None => return false,
+		};
+
+		match self.formula
+		{
+			Formula::Predicate(_)
+			| Formula::Boolean(_)
+			| Formula::Compare(_)
+			| Formula::Not(_)
+			| Formula::Exists(_)
+			| Formula::ForAll(_)
+				=> false,
+			Formula::And(formulas)
+			| Formula::Or(formulas)
+			| Formula::IfAndOnlyIf(formulas) if formulas.len() <= 1
+				=> false,
+			Formula::And(_) => match *parent_formula
+			{
+				Formula::Not(_)
+				| Formula::Exists(_)
+				| Formula::ForAll(_)
+					=> true,
+				_ => false,
+			},
+			Formula::Or(_) => match *parent_formula
+			{
+				Formula::Not(_)
+				| Formula::Exists(_)
+				| Formula::ForAll(_)
+				| Formula::And(_)
+					=> true,
+				_ => false,
+			},
+			Formula::Implies(crate::Implies{direction, ..}) => match &*parent_formula
+			{
+				Formula::Not(_)
+				| Formula::Exists(_)
+				| Formula::ForAll(_)
+				| Formula::And(_)
+				| Formula::Or(_)
+					=> true,
+				Formula::Implies(crate::Implies{direction: parent_direction,
+					antecedent: parent_antecedent, ..}) =>
+					if direction == parent_direction
+					{
+						// Implications with the same direction nested on the antecedent side require
+						// parentheses because implication is considered right-associative
+						std::ptr::eq(self.formula, &**parent_antecedent)
+					}
+					else
+					{
+						true
+					},
+				_ => false,
+			},
+			Formula::IfAndOnlyIf(_) => match *parent_formula
+			{
+				Formula::Not(_)
+				| Formula::Exists(_)
+				| Formula::ForAll(_)
+				| Formula::And(_)
+				| Formula::Or(_)
+				| Formula::Implies(_)
+					=> true,
+				_ => false,
+			},
+		}
+	}
+}
+
 fn display_formula<'formula>(formula: &'formula crate::Formula,
 	parent_formula: Option<&'formula crate::Formula>)
 	-> FormulaDisplay<'formula>
@@ -121,11 +128,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		let requires_parentheses = match self.parent_formula
-		{
-			Some(ref parent_formula) => requires_parentheses(self.formula, parent_formula),
-			None => false,
-		};
+		let requires_parentheses = self.requires_parentheses();
 
 		if requires_parentheses
 		{