Matrix and vector notation #
This file includes
simp lemmas for applying operations in
Data.Matrix.Basic to values built out
of the matrix notation
![a, b] = vecCons a (vecCons b vecEmpty) defined in
Implementation notes #
simp lemmas require that one of the arguments is of the form
vecCons _ _.
simp works with entries only when (some) entries are already given.
In other words, this notation will only appear in the output of
simp if it
already appears in the input.
This file provide notation
!![a, b; c, d] for matrices, which corresponds to
Matrix.of ![![a, b], ![c, d]].
TODO: until we implement a
Matrix.of, the pretty-printer will
!! notation, instead showing the version with
Examples of usage can be found in the
Matrices can be reflected whenever their entries can. We insert a
prevent immediate decay to a function.
Updating a row then removing it is the same as removing it.
Updating a column then removing it is the same as removing it.