Cleans up code

README.md

@@ -32,11 +32,11 @@ FA(x, F(f(x)) >> F(x))
 
 Alternatively, the `expr(formula)` function can be used, which parses a formula in standard mathematical notation. For example:
 ```
-(A ∧ B) ∨ (C → ¬D)
+F ∧ G ∨ (C → ¬D)
 F /\ G \/ (C -> ~D)
 F & G | (C -> -D)
 ⊤ ∧ ⊥
-top & bot
+top /\ bot
 F -> G -> H
 A x. F(x) /\ G(x)
 ∀x. F(x) /\ G(x)

pyprover-source/constants.coco

@@ -19,7 +19,7 @@ def first_encodeable(symbols):
 
 # Installation:
 
-version = "0.3.0"
+version = "0.3.1"
 requirements = []
 classifiers = [
     "Development Status :: 3 - Alpha",
@@ -30,10 +30,10 @@ classifiers = [
 
 # Symbols:
 
-all_top_syms = "\u22a4", "\u252c", "-T-", "top", "true"
+all_top_syms = "\u22a4", "\u252c", "top", "true"
 top_sym = all_top_syms |> first_encodeable
 
-all_bot_syms = "\u22a5", "\u2534", "_|_", "bot", "false"
+all_bot_syms = "\u22a5", "\u2534", "bot", "_|_", "false"
 bot_sym = all_bot_syms |> first_encodeable
 
 all_not_syms = "\xac", "~", "-"
@@ -48,8 +48,8 @@ and_sym = all_and_syms |> first_encodeable
 all_or_syms = "\u2228", "\\/", "|"
 or_sym = all_or_syms |> first_encodeable
 
-all_forall_syms = "\u2200", "A:", "FA ", "A ", "FA:"
+all_forall_syms = "\u2200", "A ", "A:", "FA ", "FA:"
 forall_sym = all_forall_syms |> first_encodeable
 
-all_exists_syms = "\u2203", "E:", "TE ", "E ", "TE:"
+all_exists_syms = "\u2203", "E ", "E:", "TE ", "TE:"
 exists_sym = all_exists_syms |> first_encodeable

pyprover/constants.py

@@ -1,6 +1,6 @@
 #!/usr/bin/env python
 # -*- coding: utf-8 -*-
-# __coconut_hash__ = 0xbc169ce2
+# __coconut_hash__ = 0xa101e163
 
 # Compiled with Coconut version 1.2.2-post_dev4 [Colonel]
 
@@ -44,10 +44,10 @@ def first_encodeable(symbols):  # line 7
 
 # Symbols:
 
-all_top_syms = "\u22a4", "\u252c", "-T-", "top", "true"  # line 33
+all_top_syms = "\u22a4", "\u252c", "top", "true"  # line 33
 top_sym = (first_encodeable)(all_top_syms)  # line 34
 
-all_bot_syms = "\u22a5", "\u2534", "_|_", "bot", "false"  # line 36
+all_bot_syms = "\u22a5", "\u2534", "bot", "_|_", "false"  # line 36
 bot_sym = (first_encodeable)(all_bot_syms)  # line 37
 
 all_not_syms = "\xac", "~", "-"  # line 39
@@ -62,8 +62,8 @@ def first_encodeable(symbols):  # line 7
 all_or_syms = "\u2228", "\\/", "|"  # line 48
 or_sym = (first_encodeable)(all_or_syms)  # line 49
 
-all_forall_syms = "\u2200", "A:", "FA ", "A ", "FA:"  # line 51
+all_forall_syms = "\u2200", "A ", "A:", "FA ", "FA:"  # line 51
 forall_sym = (first_encodeable)(all_forall_syms)  # line 52
 
-all_exists_syms = "\u2203", "E:", "TE ", "E ", "TE:"  # line 54
+all_exists_syms = "\u2203", "E ", "E:", "TE ", "TE:"  # line 54
 exists_sym = (first_encodeable)(all_exists_syms)  # line 55

setup.coco

@@ -13,7 +13,7 @@ from pyprover.constants import (
 setuptools.setup(
     name="pyprover",
     version=version,
-    description="A resolutional theorem prover for predicate logic in pure Python.",
+    description="Resolution theorem proving for predicate logic in pure Python.",
     url="https://github.com/evhub/pyprover",
     author="Evan Hubinger",
     author_email="evanjhub@gmail.com",

setup.py

@@ -1,6 +1,6 @@
 #!/usr/bin/env python
 # -*- coding: utf-8 -*-
-# __coconut_hash__ = 0x80ba116
+# __coconut_hash__ = 0x14015555
 
 # Compiled with Coconut version 1.2.2-post_dev4 [Colonel]
 
@@ -465,4 +465,4 @@ def consume(iterable, keep_last=0):
 from pyprover.constants import requirements  # line 6
 from pyprover.constants import classifiers  # line 7
 
-setuptools.setup(name="pyprover", version=version, description="A resolutional theorem prover for predicate logic in pure Python.", url="https://github.com/evhub/pyprover", author="Evan Hubinger", author_email="evanjhub@gmail.com", packages=setuptools.find_packages(), install_requires=requirements, classifiers=classifiers)  # line 13
+setuptools.setup(name="pyprover", version=version, description="Resolution theorem proving for predicate logic in pure Python.", url="https://github.com/evhub/pyprover", author="Evan Hubinger", author_email="evanjhub@gmail.com", packages=setuptools.find_packages(), install_requires=requirements, classifiers=classifiers)  # line 13