egison-5.1.0: lib/math/geometry/3d-euclidean-space.egi
def coordinates {Ring a} : Vector a := [x, y, z]
def metric {Ring a} : Matrix a :=
generateTensor
(\match as list integer with
| [$n, #n] -> 1
| _ -> 0)
[3, 3]
def coordinates {Ring a} : Vector a := [x, y, z]
def metric {Ring a} : Matrix a :=
generateTensor
(\match as list integer with
| [$n, #n] -> 1
| _ -> 0)
[3, 3]