 The data type LinearAlgebraTraits_d encapsulates two classes Matrix , Vector and many functions of basic linear algebra. An instance of data type Matrix is a matrix of variables of type NT . Accordingly, Vector implements vectors of variables of type NT . Most functions of linear algebra are checkable, i.e., the programs can be asked for a proof that their output is correct. For example, if the linear system solver declares a linear system \( A x = b\) unsolvable it also returns a vector \( c\) such that \( c^T A = 0\) and \( c^T b \neq 0\). More...
