Spaces:

Tonic
/

Math

Running on Zero

Tonic commited on 7 days ago

Commit

d0b4b02

verified ·

1 Parent(s): 5289607

Update app.py

Files changed (1) hide show

app.py CHANGED Viewed

@@ -9,7 +9,7 @@ LEAN4_DEFAULT_HEADER = (
     "import Mathlib\n"
     "import Aesop\n\n"
     "set_option maxHeartbeats 0\n\n"
-    "open BigOperators Real Nat Topology Rat"
 )
 title = """# 🙋🏻‍♂️Welcome to🌟Tonic's🔮Goedel Prover📉

     "import Mathlib\n"
     "import Aesop\n\n"
     "set_option maxHeartbeats 0\n\n"
+    "open BigOperators Real Nat Topology Rat\n"
 )
 title = """# 🙋🏻‍♂️Welcome to🌟Tonic's🔮Goedel Prover📉