Test for added to close a pr; space removed from tests

src/types/algebras/worlds.jl

@@ -1,6 +1,6 @@
 """
 Some worlds (dimensional worlds) can be interpreted on dimensional data,
-that is, n-dimensional arrays. The compatibility of a given world with respect of a 
+that is, n-dimensional arrays. The compatibility of a given world with respect of a
 structure of a given dimensionality must be specified via the following trait:
 
     goeswithdim(w::AbstractWorld, d) = goeswithdim(typeof(w), d)

test/check/propositional.jl

@@ -108,7 +108,7 @@ t2 = @test_nowarn TruthDict(Pair{Real,Bool}[1.0 => true, 2 => true, 3 => true])
 @test interpret(Atom("r"), DefaultedTruthDict(["p", "q"])) |> isbot
 
 
-#  normalization: negations compression ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+# normalization: negations compression ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 @test syntaxstring(normalize(parseformula("¬¬ p"))) == "p"
 @test syntaxstring(normalize(parseformula("¬¬¬ p"))) == "¬p"

test/normalize.jl

@@ -72,6 +72,9 @@ end
 @test_nowarn normalize(parseformula("(⟨G⟩A ∧ ¬⟨G⟩(A ∧ ⟨A̅⟩C))"), prefer_implications = true)
 @test_nowarn normalize(parseformula("(⟨G⟩A ∧ ¬⟨G⟩(A ∧ ⟨A̅⟩C))"), prefer_implications = true)
 
+@test "(b∧a)∨(d∧c)" |> parseformula |> normalize ==
+    "(d∧c)∨(a∧b)" |> parseformula |> normalize
+
 # φ = parseformula("(¬((q → p) → (q ∨ q))) → ⊤")
 # [check(φ, K, w; perform_normalization = false) for w in worlds]
 # φ = parseformula("¬(¬(¬(¬q ∨ p) ∨ (q ∨ q))) ∨ ⊤")