From cabe9f41850e7dd100a17153989a97a45d178da5 Mon Sep 17 00:00:00 2001 From: cyfraeviolae Date: Mon, 17 May 2021 06:49:11 -0400 Subject: examples --- app/Web.hs | 8 +++----- 1 file 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]) -- cgit v1.2.3