chore: remove stopgap prefix notation ToString instance for Prop'

Author: Will Bradley

LogicFormalization/Chapter2/Section1/NormalForms.lean

@@ -98,13 +98,6 @@ def conjNF' (p: Prop' A): Prop' A :=
     |>.map disj
     |> conj
 
-open Notation in
-#eval do
-  let p := P![(¬@'a' ∨ @'b') ∧ ¬@'c' ∧ ⊤]
-  println! p
-  println! (disjNF p, disjNF' p)
-  println! (conjNF p, conjNF' p)
-
 namespace List
 variable {α: Type u} {β: Type v} {l₁ l₂: List (List α)} {pred: List α → Bool}
 

LogicFormalization/Chapter2/Section1/Prop'.lean

@@ -16,19 +16,6 @@ namespace Prop'
 
 variable {A: Type u}
 
--- TODO: maybe put this somewhere else?
--- also TODO: replace with a proper delaborator at some point
-instance [ToString A]: ToString (Prop' A) where
-  toString := go
-  where go -- prefix notation
-    | .atom a => toString a
-    | .true => "⊤"
-    | .false => "⊥"
-    | .not p => s!"¬{go p}"
-    | .or p q => s!"∨{go p}{go q}"
-    | .and p q => s!"∧{go p}{go q}"
-
-
 @[reducible]
 def length: Prop' A → ℕ
 | .atom _ | .true | .false => 1