use new syntax

algebra/field.math

@@ -21,7 +21,7 @@ when:
 . 'F is \field'
 . 'x [.in.]: F'
 means: 'y [.in.]: F'
-expresses:
+expressing:
 . 'x * y = 1'
 . 'y * x = 1'
 Documented:

algebra/group.math

@@ -5,7 +5,7 @@
 [\group]
 Describes: G := (X, *, e)
 extends: 'G is \monoid'
-specifies:
+satisfying:
 . [existence.of.inverses]
   forAll: x
   where: 'x [.in.]: G'
@@ -31,7 +31,7 @@ extends: 'x is \monoid.element:of{G}'
 Provides:
 . symbol: 'x.inv :=> \group.inverse:of{x}:in{G}'
   written: "{x?}^{-1}"
-. symbol: 'x :^ n :=> x \{group.power}/ n'
+. symbol: 'x :^ n :=> x \.group.power./ n'
   written: "{x?}^{n?}"
 Documented:
 . called: "element of group G?"
@@ -56,6 +56,7 @@ extends: 'Y is \set'
 specifies:
 . 'Y [.subset.]: X'
 . 'Y is \non.empty.set'
+satisfying:
 . forAll: x, y
   where: 'x, y [.in.]: Y'
   then: 'x *_0 y := x * y'
@@ -71,12 +72,12 @@ Documented:
 Id: "c12a4601-5513-42b6-97e3-19e64896b14f"
 
 
-[H := (X, *, e) \[subgroup]/ G]
+[H := (X, *, e) \.subgroup./ G]
 States:
 when:
 . 'G is \group'
 . 'X is \set'
-that: 'H is \subgroup:of{G}'
+specifies: 'H is \subgroup:of{G}'
 Documented:
 . written: "H? \leq G?"
 ------------------------------------------
@@ -86,7 +87,7 @@ Id: "8b8b2238-a9bb-44e4-a4aa-b7857fbd9d51"
 Theorem:
 given: G, H
 where: 'G is \group'
-suchThat: 'H \[subgroup]/ G'
+suchThat: 'H \.subgroup./ G'
 then: 'H is \group'
 ------------------------------------------
 Id: "6fe2d452-6b58-442e-920b-f273fac1b3b9"
@@ -99,7 +100,7 @@ when:
 . 'G is \group'
 . 'x [.in.]: G'
 means: 'y [.in.]: G'
-expresses:
+expressing:
 . 'x * y = e'
 . 'y * x = e'
 Justified:
@@ -112,35 +113,35 @@ Aliases:
 Id: "2293a62b-71a4-431e-82a1-c7613a52267f"
 
 
-[x \{group.power}/ n]
+[x \.group.power./ n]
 Defines: y
 using: G := (X, *, e)
 when:
 . 'G is \group'
 . 'x [.in.]: G'
 . 'n is \natural'
 means: 'y [.in.]: G'
-expresses:
+expressing:
 . piecewise:
   if: 'n = 0'
   then: 'y = e'
   elseIf:
   . exists: m
     where: 'm is \natural'
     suchThat: 'n = m++'
-  then: 'y = x * (x \{group.power}/ m)'
+  then: 'y = x * (x \.group.power./ m)'
 Documented:
 . called: "x? raised to the power n?"
 . written: "{x?}^{n?}"
 ------------------------------------------
 Id: "1aaf732a-1987-4ee2-860e-98adf261b5f6"
 
 
-[G1 := (X1, *_1, e1) \{group.direct.product}/ G2 := (X2, *_2, e2)]
+[G1 := (X1, *_1, e1) \.group.direct.product./ G2 := (X2, *_2, e2)]
 Defines: H := (Y, +, u)
 when: 'G1, G2 is \group'
-expresses:
-. 'Y := X1 \{set.times}/ X2'
+specifies:
+. 'Y := X1 \.set.times./ X2'
 . 'u := (e1, e2)'
 Documented:
 . called: "direct product of the groups G1? and G2?"
@@ -163,7 +164,7 @@ Id: "bba5ed08-adfd-4465-8192-d60f2998a271"
 [\abelian.group]
 Describes: G
 extends: 'G is \group'
-specifies:
+satisfying:
 . forAll: x, y
   where: 'x, y [.in.]: G'
   then: 'x * y = y * x'
@@ -222,8 +223,9 @@ Id: "6dcccfc0-be83-489a-9c2e-040e61bce8f7"
 Defines: k
 when: 'P is \\formulation{statement}'
 means: 'k is \natural'
-expresses:
+specifies:
 . 'P(k) is \\true'
+expressing:
 . not:
   . exists: j
     where: 'j is \natural'
@@ -242,7 +244,7 @@ when:
 . 'G is \group'
 . 'n is \natural'
 means: 'n is \natural'
-expresses:
+specifies:
 . 'n := \smallest.natural:suchThat[k]{x^k = e}'
 Documented:
 . called: "\textrm{order of } x? \textrm{ in group } G?"

algebra/module.math

@@ -8,7 +8,8 @@ when: 'R0 is \ring'
 extends: 'G is \group'
 specifies:
 . 'R := R0'
-. '"*" is \function:on{R {.times.} G}:to{G}'
+. '"*" is \function:on{R [.times.] G}:to{G}'
+satisfying:
 . [scalar.multiplication]
   forAll: r, s, x, y
   where:
@@ -51,7 +52,7 @@ Id: "b31db455-e075-4e67-823e-65d76087290a"
 Describes: M
 when: 'R is \ring.with.identity'
 extends: 'M is \left.module:over{R}'
-specifies:
+satisfying:
 . forAll: x
   where: 'x [.in.]: M'
   then: 'R.1 * x = x'
@@ -78,7 +79,8 @@ when: 'R0 is \ring'
 extends: 'G is \group'
 specifies:
 . 'R := R0'
-. '"*" is \function:on{G {.times.} R}:to{G}'
+. '"*" is \function:on{G [.times.] R}:to{G}'
+satisfying:
 . [scalar.multiplication]
   forAll: r, s, x, y
   where:
@@ -121,7 +123,7 @@ Id: "d8a4d363-63ff-4bc4-b0d1-60336739c587"
 Describes: M
 when: 'R is \ring.with.identity'
 extends: 'M is \right.module:over{R}'
-specifies:
+satisfying:
 . forAll: x
   where: 'x [.in.]: M'
   then: 'x * R.1  = x'
@@ -181,7 +183,7 @@ Theorem:
 given: M := (R, G, *), *_0
 where:
 . 'M is \left.module'
-. '"*_0" is \function:on{M {.times.} R}:to{M}'
+. '"*_0" is \function:on{M [.times.] R}:to{M}'
 suchThat:
 . forAll: m, r
   where:

algebra/monoid.math

@@ -7,6 +7,7 @@ Describes: M := (X, *, e)
 extends: '(X, "*") is \semigroup'
 specifies:
 . 'e [.in.]: M'
+satisfying:
 . forAll: x
   where: 'x [.in.]: M'
   then:

algebra/operations.math

@@ -16,7 +16,7 @@ Id: "0b0939af-e4a8-4c4d-b8fc-beba6a9e516c"
 Describes: x * y
 when: 'X is \set'
 extends: '"*" is \binary.operation:on{X}'
-specifies:
+satisfying:
 . forAll: x, y, z
   where: 'x, y, z [.in.]: X'
   then: 'x * (y * z) = (x * y) * z'
@@ -30,7 +30,7 @@ Id: "4e45d31a-56d0-452c-8a94-38c09335cf2b"
 Describes: x * y
 when: 'X is \set'
 extends: '"*" is \binary.operation:on{X}'
-specifies:
+satisfying:
 . forAll: x, y
   where: 'x, y [.in.]: X'
   then: 'x * y = y * x'
@@ -45,7 +45,7 @@ Describes: x * y
 using: X
 when: 'Y [.subset.]: X'
 extends: '"*" is \binary.operation:on{X}'
-specifies:
+satisfying:
 . forAll: a, b
   where: 'a, b [.in.]: Y'
   then: 'a * b [.in.]: Y'

algebra/quasigroup.math

@@ -5,7 +5,7 @@
 [\quasigroup]
 Describes: Q := (X, *)
 extends: 'Q is \magma'
-specifies:
+satisfying:
 . [latin.square.property]
   forAll: a, b
   where: 'a, b [.in.]: Q'

algebra/ring.math

@@ -8,7 +8,7 @@ Describes: R := (X, +, *, 0)
 extends:
 . '(X, "+", 0) is \abelian.group'
 . '(X, "*") is \semigroup'
-specifies:
+satisfying:
 . [distributive.law]
   forAll: x, y, z
   where: 'x, y, z [.in.]: R'
@@ -60,7 +60,7 @@ Id: "7e9002e6-4aa3-4312-b113-798474c70e0f"
 [\commutative.ring]
 Describes: R
 extends: 'R is \ring'
-specifies:
+satisfying:
 . forAll: x, y
   where: 'x, y [.in.]: R'
   then: 'x * y = y * x'
@@ -82,7 +82,7 @@ Id: "57d40c75-7b95-4680-ac65-414efa306beb"
 [\trivial.ring]
 Defines: R := (X, +, *, 0)
 means: 'R is \ring'
-expresses:
+expressing:
 . 'x + y := 0'
 . 'x * y := 0'
 . 'X := \set:from{0}'
@@ -97,7 +97,7 @@ Id: "bcff7894-7ec2-44eb-ae00-6e445ef19c9a"
 [\nontrivial.ring]
 Describes: R
 extends: 'R is \ring'
-specifies: 'R != \trivial.ring'
+satisfying: 'R != \trivial.ring'
 Documented:
 . called: "non-trivial ring"
 ------------------------------------------
@@ -107,7 +107,7 @@ Id: "029fa21a-8527-4a08-9035-d5a29d8014f6"
 [\division.ring]
 Describes: R
 extends: 'R is \ring.with.identity'
-specifies:
+satisfying:
 . '0 != 1'
 . forAll: x
   where: 'x [.in.]: R'

analysis/metric_space.math

@@ -5,8 +5,8 @@
 [\metric:on{X}]
 Describes: d(x, y)
 when: 'X is \set'
-extends: 'd is \function:on{X {.times.} X}:to{\reals}'
-specifies:
+extends: 'd is \function:on{X [.times.] X}:to{\reals}'
+satisfying:
 . forAll: x
   where: 'x [.in.]: X'
   then: 'd(x, x) = 0'

function.math

@@ -1,4 +1,4 @@
-::function.on.A.to.B
+::[function.on.A.to.B]
 
 ## Functions
 
@@ -13,6 +13,7 @@ when: 'A, B is \set'
 specifies:
 . 'x [.in.]: A'
 . 'f(x) [.in.]: B'
+satisfying:
 . forAll: a
   where: 'a [.in.]: A'
   then:
@@ -27,7 +28,7 @@ Documented:
 Id: "dd66298e-4e01-400b-897b-712c4c0892a1"
 
 
-::injective.function
+::[injective.function]
 
 ## Injective Functions
 
@@ -42,7 +43,7 @@ Note: These types of functions are also said to be *one-to-one*.
 Describes: f(x)
 when: 'A, B is \set'
 extends: 'f is \function:on{A}:to{B}'
-specifies:
+satisfying:
 . forAll: x1, x2
   where: 'x1, x2 [.in.]: A'
   then:
@@ -58,7 +59,7 @@ Documented:
 Id: "84e7fd56-af43-441b-bc58-8b6093b14443"
 
 
-::surjective.function
+::[surjective.function]
 
 Similarly, in general, for the function $f$ where $f$ is a function on $A$ to
 $B$ it is possible for there to be an element $b \in B$ such that there doesn't
@@ -77,7 +78,7 @@ element.  Surjective functions are also said to be *onto*.
 Describes: f(x)
 when: 'A, B is \set'
 extends: 'f is \function:on{A}:to{B}'
-specifies:
+satisfying:
 . forAll: b
   where: 'b [.in.]: B'
   then:
@@ -123,7 +124,7 @@ Defines: g(x)
 using: A, B
 when: 'f is \function:on{A}:to{B}'
 means: 'g is \function:on{B}:to{A}'
-expresses:
+expressing:
 . forAll: a
   where: 'a [.in.]: A'
   then: 'g(f(a)) = a'
@@ -143,14 +144,14 @@ functions.
 ::
 
 
-[f \{function.compose}/ g]
+[f \.function.compose./ g]
 Defines: h(x)
 using: A, B, C
 when:
 . 'g is \function:on{A}:to{B}'
 . 'f is \function:on{B}:to{C}'
 means: 'h is \function:on{A}:to{C}'
-expresses: 'h(x) := f(g(x))'
+expressing: 'h(x) := f(g(x))'
 Documented:
 . written: "f+? \circ g+?"
 . called: "function composition"
@@ -169,7 +170,7 @@ structure.
 Defines: f(x)
 when: 'A is \set'
 means: 'f is \function:on{A}:to{A}'
-expresses: 'f(x) := x'
+expressing: 'f(x) := x'
 Documented:
 . written: "\textrm{id}_{A?}"
 . called: "identify function on $A?$"

integers.math

@@ -14,7 +14,7 @@ Id: "67ba0d5c-d30c-4c1f-85e0-60b9efba44d5"
 [\integer.set]
 Defines: X
 means: 'X is \set'
-expresses: 'X := \set:of[x]{x | x is \integer}'
+expressing: 'X := \set:of[x]{x | x is \integer}'
 Documented:
 . written: "\mathbb{Z}"
 ------------------------------------------
@@ -24,7 +24,7 @@ Id: "5f310f77-f89c-4094-8b39-aab057b03720"
 [\integers]
 Defines: Z := (X, +, *, 0, 1)
 means: 'X is \set'
-expresses: 'X := \integer.set'
+expressing: 'X := \integer.set'
 Provides: 'x [.in.]: Z :-> x [.in.]: X'
 Documented:
 . written: "\mathbb{Z}"