summaryrefslogtreecommitdiff
path: root/app/Web.hs
diff options
context:
space:
mode:
Diffstat (limited to 'app/Web.hs')
-rw-r--r--app/Web.hs2
1 files changed, 1 insertions, 1 deletions
diff --git a/app/Web.hs b/app/Web.hs
index ba54f85..89b6ac5 100644
--- a/app/Web.hs
+++ b/app/Web.hs
@@ -97,7 +97,7 @@ examples =
[ ("1+1=2", "one plus one equals two."),
("Ax.Ay.x+y=y+x", "addition is commutative."),
("Ex.Ay.x>y", "there exists a largest natural."),
- ("Ee.Ax.(x+e=x & Ay.(x+y=x -> e=y))", "the additive identity exists and is unique."),
+ ("Ee.Ae'.(Ax.e'+x=x <-> e=e')", "the additive identity exists and is unique."),
("Ax.Ey.2y=x", "every natural is even."),
("Ax.Ey.(2y=x | 2y+1=x)", "every natural is either even or odd."),
("Ax.Ay.Az.((x=y & y=z) -> x=z)", "equality is transitive."),