Real number grids

Uses
- Real numbers
- Integer grids

Real number grids have sort ℝ⧺ℝ.p⧺ℝ and are defined using the operator
 ℝ⧺ℝ.p ⧺ ℝ : ℝ⧺ℝ.p⧺ℝ
The first argument of this operator is constructed using the auxiliary operator
 ℝ ⧺ ℝ.p : ℝ⧺ℝ.p of sort ℝ⧺ℝ.p, with ℤ⧺ℕ.nz ⊆ ℝ⧺ℝ.p.

Integer grids are a special case of real number grids:
 ℤ⧺ℕ.nz⧺ℤ ⊆ ℝ⧺ℝ.p⧺ℝ

Another special case are rational number grids:
 ℚ⧺ℚ.p⧺ℚ ⊆ ℝ⧺ℝ.p⧺ℝ
of sort ℚ⧺ℚ.p⧺ℚ, with ℤ⧺ℕ.nz⧺ℤ ⊆ ℚ⧺ℚ.p⧺ℚ.
They are defined using the operator
 ℚ⧺ℚ.p ⧺ ℚ : ℚ⧺ℚ.p⧺ℚ
with the auxiliary operator
 ℚ ⧺ ℚ.p : ℚ⧺ℚ.p
of sort ℚ⧺ℚ.p, with ℤ⧺ℕ.nz ⊆ ℚ⧺ℚ.p and ℚ⧺ℚ.p ⊆ ℝ⧺ℝ.p.