fix(Main)

FormalMathematicsLab · Sep 3, 2023 · 7f7d161 · 7f7d161
1 parent bc98adb
commit 7f7d161
Showing 1 changed file with 0 additions and 8 deletions.
diff --git a/Main.lean b/Main.lean
@@ -1,9 +1 @@
 import «Logic»
-
-open FirstOrder
-
-def d : FirstOrder.Derivation₁ (L := (Language.relational (fun _ => ℕ)))
-    “(([Language.toRelational 0]() → [Language.toRelational 1]()) → [Language.toRelational 0]()) → [Language.toRelational 0]()” := by proveDerivation₁
-
-unsafe def main : IO Unit :=
-  IO.println s!"{repr d}"