diff options
author | cyfraeviolae <cyfraeviolae> | 2021-05-18 19:35:59 -0400 |
---|---|---|
committer | cyfraeviolae <cyfraeviolae> | 2021-05-18 19:35:59 -0400 |
commit | b66ac09af03b69d409df27ef32c90fa38924af2f (patch) | |
tree | 1c5268c5ef9d56e5ab07b7538d2e3ba0ab611f99 /app | |
parent | cabe9f41850e7dd100a17153989a97a45d178da5 (diff) |
fix additive identity example
Diffstat (limited to 'app')
-rw-r--r-- | app/Web.hs | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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."), |