| 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...
|