Dropping parentheses

input-output-hk · Oct 1, 2024 · c5c87af · c5c87af
1 parent dfdb3d5
commit c5c87af
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/Peras/Conformance/Soundness.agda b/src/Peras/Conformance/Soundness.agda
@@ -420,10 +420,10 @@ module _ ⦃ _ : Hashable (List Tx) ⦄
                           → transition p (modelState s₀) (NewChain chain) ≡ Just ((cs , vs) , ms₁)
                           → Soundness s₀ ms₁ (map (State.clock s₀ ,_) vs)
     newChain-soundness s₀ (block ∷ rest) inv prf
-      with (slotNumber block == State.clock s₀) in checkSlot
+      with slotNumber block == State.clock s₀ in checkSlot
          | checkBlockFromOther block in checkedOther
-         | (parentBlock block == tipHash rest) in checkHash
-         | (rest == pref (modelState s₀)) in checkRest
+         | parentBlock block == tipHash rest in checkHash
+         | rest == pref (modelState s₀) in checkRest
          | checkSignedBlock block in checkedSig
          | checkLeadershipProof (leadershipProof block) in checkedLead
          | lastSlot rest Haskell.< slotNumber block in checkedNewer