diff options
| -rw-r--r-- | app/Web.hs | 8 |
1 files changed, 3 insertions, 5 deletions
@@ -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]) |