summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--app/Web.hs8
1 files changed, 3 insertions, 5 deletions
diff --git a/app/Web.hs b/app/Web.hs
index 7f7c2ba..ba54f85 100644
--- a/app/Web.hs
+++ b/app/Web.hs
@@ -95,17 +95,15 @@ homeURI f = "/" <> toUrlPiece (safeLink api (Proxy :: Proxy HomeAPI) f :: Link)
examples :: [(String, String)]
examples =
[ ("1+1=2", "one plus one equals two."),
- ("Ax.Ax'.x+x'=x'+x", "addition is commutative."),
- ("Ee.Ax.x+e=x", "there exists an additive identity."),
+ ("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."),
("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."),
("Ax.Ay.(x<=y <-> y<=x)", "less-than-or-equal-to is symmetric."),
("Ax.Ay.((x<=y & y<=x) -> x=y)", "less-than-or-equal-to is antisymmetric."),
- ("Ax.Ay.(x+1=y+1 -> x=y)", "the successor function is injective."),
- ("Ax.x+1!=0", "there is no natural whose successor is zero."),
- ("(Ax.x=x & Ex.x=0 & Ex.x=1)", "the Sphinx is not an acolyte of prenex normal form.")
+ ("Ax.Ay.(x+1=y+1 -> x=y)", "the successor function is injective.")
]
styles :: HomeView -> (String, String, [Attribute])